diff --git a/Induction/Structural/Types.hs b/Induction/Structural/Types.hs
--- a/Induction/Structural/Types.hs
+++ b/Induction/Structural/Types.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TemplateHaskell, FlexibleContexts #-}
+{-# LANGUAGE TemplateHaskell, FlexibleContexts, DeriveFunctor #-}
 -- | Types
 module Induction.Structural.Types
     (
@@ -37,7 +37,7 @@
     | Con c [Term c v]
     | Fun v [Term c v]
     -- ^ Induction on exponential data types yield assumptions with functions
-  deriving (Eq,Ord)
+  deriving (Eq,Ord,Functor)
 
 -- Typed variables are represented as (v,t)
 
@@ -80,6 +80,7 @@
     , conclusion :: Predicate c v
     -- ^ The induction conclusion
     }
+    deriving (Functor)
 
 -- | Quantifier lists are represented as tuples of variables and their type.
 --
diff --git a/changelog b/changelog
--- a/changelog
+++ b/changelog
@@ -1,3 +1,6 @@
+structural-induction 0.3 (released 2015-06-30)
+	* Add Functor instance for Term and Obligation.
+
 structural-induction 0.2.0.1 (released 2015-06-10)
 	* Add missing test suite files to extra-source-files.
 
diff --git a/structural-induction.cabal b/structural-induction.cabal
--- a/structural-induction.cabal
+++ b/structural-induction.cabal
@@ -1,6 +1,6 @@
 name:               structural-induction
 category:           Theorem Provers, Logic
-version:            0.2.0.1
+version:            0.3
 license:            LGPL-3
 license-file:       LICENSE
 author:             Dan Rosén