diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,6 +1,6 @@
 term-rewriting library -- basic first order term rewriting.
 
-Copyright (c) 2011-2013 by Martin Avanzini, Bertram Felgenhauer and
+Copyright (c) 2011-2017 by Martin Avanzini, Bertram Felgenhauer and
 Christian Sternagel.
 
 Permission is hereby granted, free of charge, to any person obtaining a
diff --git a/src/Data/Rewriting/Problem/Type.hs b/src/Data/Rewriting/Problem/Type.hs
--- a/src/Data/Rewriting/Problem/Type.hs
+++ b/src/Data/Rewriting/Problem/Type.hs
@@ -9,10 +9,15 @@
   RulesPair (..),
   Problem (..),
   Theory (..),
-  allRules
+  allRules,
+  map
  ) where
 
+import Prelude hiding (map)
+import qualified Prelude as P
+
 import Data.Rewriting.Rule (Rule (..))
+import qualified Data.Rewriting.Rule as Rule
 
 data StartTerms = AllTerms
                 | BasicTerms deriving (Eq, Show)
@@ -38,3 +43,23 @@
 
 allRules :: RulesPair f v -> [Rule f v]
 allRules rp = strictRules rp ++ weakRules rp
+
+map :: (f -> f') -> (v -> v') -> Problem f v -> Problem f' v'
+map ffun fvar prob = 
+   Problem { startTerms = startTerms prob 
+           , strategy = strategy prob
+           , theory = P.map (mapTheory ffun fvar) <$> theory prob 
+           , rules = mapRulesPair ffun fvar (rules prob)
+           , variables = P.map fvar (variables prob)
+           , symbols = P.map ffun (symbols prob)
+           , comment = comment prob}
+              
+mapTheory :: (f -> f') -> (v -> v') -> Theory f v -> Theory f' v'
+mapTheory ffun _ (SymbolProperty p fs) = SymbolProperty p (P.map ffun fs)
+mapTheory ffun fvar (Equations rs) = Equations (P.map (Rule.map ffun fvar) rs)
+
+mapRulesPair :: (f -> f') -> (v -> v') -> RulesPair f v -> RulesPair f' v'
+mapRulesPair ffun fvar rp = 
+    RulesPair { strictRules = modify (strictRules rp)
+              , weakRules = modify (weakRules rp)}
+        where modify = P.map (Rule.map ffun fvar)
diff --git a/src/Data/Rewriting/Rule/Ops.hs b/src/Data/Rewriting/Rule/Ops.hs
--- a/src/Data/Rewriting/Rule/Ops.hs
+++ b/src/Data/Rewriting/Rule/Ops.hs
@@ -47,10 +47,10 @@
 right f = f . rhs
 
 
--- | Lifting of 'Term.rename' to 'Rule': renames left- and
--- right-hand sides.
+-- | Lifting of 'Term.rename' to 'Rule': renames left- and right-hand sides.
+-- 
 -- >>> rename (+ 1) $ Rule {lhs = (Fun 'f' [Var 1, Fun 'g' [Var 2]]), rhs = Fun 'g' [Var 1]}
--- Rule {lhs = (Fun 'f' [Var 2, Fun 'g' [Var 3]]), rhs = Fun 'g' [Var 2]}
+-- Rule {lhs = Fun 'f' [Var 2, Fun 'g' [Var 3]], rhs = Fun 'g' [Var 2]}
 rename :: (v -> v') -> Rule f v -> Rule f v'
 rename f rl = Rule (left (Term.rename f) rl) (right (Term.rename f) rl)
 
diff --git a/src/Data/Rewriting/Rule/Type.hs b/src/Data/Rewriting/Rule/Type.hs
--- a/src/Data/Rewriting/Rule/Type.hs
+++ b/src/Data/Rewriting/Rule/Type.hs
@@ -6,14 +6,22 @@
 module Data.Rewriting.Rule.Type (
     module Data.Rewriting.Term.Type,
     Rule (..),
+    map,
+    mapSides
 ) where
 
+import Prelude hiding (map)
 import Data.Rewriting.Term.Type hiding (map, fold)
+import qualified Data.Rewriting.Term.Type as T
 
 -- | Rewrite rule with left-hand side and right-hand side.
 data Rule f v = Rule { lhs :: Term f v, rhs :: Term f v }
     deriving (Ord, Eq, Show)
 
--- mapRule :: (Term f v -> Term f' v') -> Rule f v -> Rule f' v'
--- mapRule f r = Rule{ lhs = f (lhs r), rhs = f (rhs r) }
+
+mapSides :: (Term f v -> Term f' v') -> Rule f v -> Rule f' v'
+mapSides f r = Rule{ lhs = f (lhs r), rhs = f (rhs r) }
+
+map :: (f -> f') -> (v -> v') -> Rule f v -> Rule f' v'
+map f v = mapSides (T.map f v)
 
diff --git a/src/Data/Rewriting/Rules/Ops.hs b/src/Data/Rewriting/Rules/Ops.hs
--- a/src/Data/Rewriting/Rules/Ops.hs
+++ b/src/Data/Rewriting/Rules/Ops.hs
@@ -11,17 +11,21 @@
     varsDL,
     lhss,
     rhss,
+    map,
     restrictFuns,
     -- * Predicates on Rules
     isLinear, isLeftLinear, isRightLinear,
     isGround, isLeftGround, isRightGround,
     isErasing,
     isCreating,
+    isExpanding,
     isDuplicating,
     isCollapsing,
     isValid,
 ) where
 
+import Prelude hiding (map)
+import qualified Prelude as P
 import Data.Rewriting.Rule (Rule)
 import Data.Rewriting.Term (Term)
 import qualified Data.Rewriting.Term as Term
@@ -30,11 +34,11 @@
 
 -- | @lhss rs@ returns the list of left-hand sides of @rs@
 lhss :: [Rule f v] -> [Term f v]
-lhss = map Rule.lhs
+lhss = P.map Rule.lhs
 
 -- | @lhss rs@ returns the list of right-hand sides of @rs@
 rhss :: [Rule f v] -> [Term f v]
-rhss = map Rule.rhs
+rhss = P.map Rule.rhs
 
 -- | Lifting of Term.'Term.funs' to list of rules.
 funs :: [Rule f v] -> [f]
@@ -48,6 +52,10 @@
 -- | Lifting of Term.'Term.vars' to list of rules.
 vars :: [Rule f v] -> [v]
 vars = flip varsDL []
+
+-- | Lifting of Rule.'Rule.map' to list of rules.
+map :: (f -> f') -> (v -> v') -> [Rule f v] -> [Rule f' v']
+map f v = P.map (Rule.map f v)
 
 -- | Difference List version of 'vars'.
 -- We have @varsDL r vs = vars r ++ vs@.
diff --git a/src/Data/Rewriting/Substitution/Pretty.hs b/src/Data/Rewriting/Substitution/Pretty.hs
--- a/src/Data/Rewriting/Substitution/Pretty.hs
+++ b/src/Data/Rewriting/Substitution/Pretty.hs
@@ -24,6 +24,3 @@
 
 instance (Pretty v, Pretty f, Pretty v') => Pretty (GSubst v f v') where
     pretty = prettyGSubst pretty pretty pretty
-
-instance (Pretty f, Pretty v) => Pretty (Subst f v) where
-    pretty = prettySubst pretty pretty
diff --git a/term-rewriting.cabal b/term-rewriting.cabal
--- a/term-rewriting.cabal
+++ b/term-rewriting.cabal
@@ -1,5 +1,5 @@
 name:          term-rewriting
-version:       0.2
+version:       0.2.1
 stability:     experimental
 author:        Martin Avanzini,
                Bertram Felgenhauer,
@@ -65,7 +65,7 @@
         Data.Rewriting.Utils.Parse
     build-depends:
         containers >= 0.3 && < 0.6,
-        multiset >= 0.2 && < 0.3,
+        multiset >= 0.2 && < 0.4,
         parsec >= 3.1.6 && < 3.2,
         union-find-array >= 0.1 && < 0.2,
         array >= 0.3 && < 0.6,