diff --git a/Setup.hs b/Setup.hs
--- a/Setup.hs
+++ b/Setup.hs
diff --git a/compdata.cabal b/compdata.cabal
--- a/compdata.cabal
+++ b/compdata.cabal
@@ -1,9 +1,9 @@
 Name:			compdata
-Version:		0.5.2
+Version:		0.5.3
 Synopsis:            	Compositional Data Types
 Description:
 
-  Based on Wouter Swierstra's Functional Pearl /Data types à la carte/
+  Based on Wouter Swierstra's Functional Pearl /Data types a la carte/
   (Journal of Functional Programming, 18(4):423-436, 2008,
   <http://dx.doi.org/10.1017/S0956796808006758>),
   this package provides a framework for defining recursive
@@ -29,7 +29,7 @@
   In concrete terms, this package provides the following features:
   .
   *  Compositional data types in the style of Wouter Swierstra's
-     Functional Pearl /Data types à la carte/.
+     Functional Pearl /Data types a la carte/.
   .
   *  Modular definition of functions on compositional data types through
      catamorphisms and anamorphisms as well as more structured
@@ -69,10 +69,12 @@
      to families of mutually recursive data types and (more generally) GADTs.
      This extension resides in the module "Data.Comp.Multi".
   .
-  *  /Parametric compositional data types/. All of the above is also lifted
-     to parametric data types, which enables support for parametric higher-order
-     abstract syntax (PHOAS). This extension resides in the module
-     "Data.Comp.Param".
+  * /Parametric compositional data types/ (Workshop on Mathematically
+     Structured Functional Programming, 3-24, 2012,
+     <http://dx.doi.org/10.4204/EPTCS.76.3>). All of the above is also
+     lifted to parametric data types, which enables support for
+     parametric higher-order abstract syntax (PHOAS). This extension
+     resides in the module "Data.Comp.Param".
   .
   *  /Generalised parametric compositional data types/. All of the above is also
      lifted to generalised parametric data types, which enables support for
@@ -291,3 +293,7 @@
     buildable:          False
   else
     Build-Depends:      base == 4.*, template-haskell, containers, mtl, QuickCheck >= 2, derive, deepseq, criterion, random, uniplate, th-expand-syns, transformers
+
+source-repository head
+  type:     hg
+  location: https://bitbucket.org/paba/compdata
diff --git a/src/Data/Comp/Algebra.hs b/src/Data/Comp/Algebra.hs
--- a/src/Data/Comp/Algebra.hs
+++ b/src/Data/Comp/Algebra.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables, TypeOperators,
+{-# LANGUAGE GADTs, Rank2Types, ScopedTypeVariables, TypeOperators,
   FlexibleContexts, CPP #-}
 --------------------------------------------------------------------------------
 -- |
diff --git a/src/Data/Comp/Annotation.hs b/src/Data/Comp/Annotation.hs
--- a/src/Data/Comp/Annotation.hs
+++ b/src/Data/Comp/Annotation.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances,
-  UndecidableInstances, RankNTypes, GADTs, ScopedTypeVariables #-}
+  UndecidableInstances, Rank2Types, GADTs, ScopedTypeVariables #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Annotation
diff --git a/src/Data/Comp/Automata.hs b/src/Data/Comp/Automata.hs
--- a/src/Data/Comp/Automata.hs
+++ b/src/Data/Comp/Automata.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE RankNTypes, FlexibleContexts, ImplicitParams, GADTs, TypeOperators #-}
+{-# LANGUAGE Rank2Types, FlexibleContexts, ImplicitParams, GADTs, TypeOperators #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Automata
@@ -102,29 +102,35 @@
 infixr 0 &
 
 -- | left-biased union of two mappings.
+
 (&) :: Ord k => Map k v -> Map k v -> Map k v
 (&) = Map.union
 
 -- | This operator constructs a singleton mapping.
+
 (|->) :: k -> a -> Map k a
 (|->) = Map.singleton
 
 -- | This is the empty mapping.
+
 o :: Map k a
 o = Map.empty
 
 -- | This function provides access to components of the states from
 -- "below".
+
 below :: (?below :: a -> q, p :< q) => a -> p
 below = pr . ?below
 
 -- | This function provides access to components of the state from
 -- "above"
+
 above :: (?above :: q, p :< q) => p
 above = pr ?above
 
 -- | Turns the explicit parameters @?above@ and @?below@ into explicit
 -- ones.
+
 explicit :: ((?above :: q, ?below :: a -> q) => b) -> q -> (a -> q) -> b
 explicit x ab be = x where ?above = ab; ?below = be
 
@@ -132,6 +138,7 @@
 -- | This type represents stateful term homomorphisms. Stateful term
 -- homomorphisms have access to a state that is provided (separately)
 -- by a bottom-up or top-down state transformation function (or both).
+                           
 type QHom f q g = forall a . (?below :: a -> q, ?above :: q) => f a -> Context g a
 
 -- -- | This type represents (pure, i.e. stateless) homomorphism by
@@ -170,12 +177,14 @@
 
 -- | This function generalises 'runUpTrans' to contexts. Therefore,
 -- additionally, a transition function for the holes is needed.
+
 runUpTrans' :: (Functor f, Functor g) => UpTrans f q g -> Context f (q,a) -> (q, Context g a)
 runUpTrans' trans = run where
     run (Hole (q,a)) = (q, Hole a)
     run (Term t) = fmap appCxt $ trans $ fmap run t
 
 -- | This function composes two DUTTs. (see TATA, Theorem 6.4.5)
+    
 compUpTrans :: (Functor f, Functor g, Functor h)
                => UpTrans g p h -> UpTrans f q g -> UpTrans f (q,p) h
 compUpTrans t2 t1 x = ((q1,q2), c2) where
@@ -184,43 +193,52 @@
 
 
 -- | This function composes a DUTT with an algebra.
+    
 compAlgUpTrans :: (Functor g)
                => Alg g a -> UpTrans f q g -> Alg f (q,a)
 compAlgUpTrans alg trans = fmap (cata' alg) . trans
 
 
 -- | This combinator composes a DUTT followed by a signature function.
+
 compSigUpTrans :: (Functor g) => SigFun g h -> UpTrans f q g -> UpTrans f q h
 compSigUpTrans sig trans x = (q, appSigFun sig x') where
     (q, x') = trans x
 
 -- | This combinator composes a signature function followed by a DUTT.
+    
 compUpTransSig :: UpTrans g q h -> SigFun f g -> UpTrans f q h
 compUpTransSig trans sig = trans . sig
 
 -- | This combinator composes a DUTT followed by a homomorphism.
+
 compHomUpTrans :: (Functor g, Functor h) => Hom g h -> UpTrans f q g -> UpTrans f q h
 compHomUpTrans hom trans x = (q, appHom hom x') where
     (q, x') = trans x
 
 -- | This combinator composes a homomorphism followed by a DUTT.
+    
 compUpTransHom :: (Functor g, Functor h) => UpTrans g q h -> Hom f g -> UpTrans f q h
 compUpTransHom trans hom x  = runUpTrans' trans . hom $ x
 
 -- | This type represents transition functions of deterministic
 -- bottom-up tree acceptors (DUTAs).
+
 type UpState f q = Alg f q
 
 -- | Changes the state space of the DUTA using the given isomorphism.
+
 tagUpState :: (Functor f) => (q -> p) -> (p -> q) -> UpState f q -> UpState f p
 tagUpState i o s = i . s . fmap o
 
 -- | This combinator runs the given DUTA on a term returning the final
 -- state of the run.
+
 runUpState :: (Functor f) => UpState f q -> Term f -> q
 runUpState = cata
 
 -- | This function combines the product DUTA of the two given DUTAs.
+
 prodUpState :: Functor f => UpState f p -> UpState f q -> UpState f (p,q)
 prodUpState sp sq t = (p,q) where
     p = sp $ fmap fst t
@@ -229,6 +247,7 @@
 
 -- | This function constructs a DUTT from a given stateful term
 -- homomorphism with the state propagated by the given DUTA.
+    
 upTrans :: (Functor f, Functor g) => UpState f q -> QHom f q g -> UpTrans f q g
 upTrans st f t = (q, c)
     where q = st $ fmap fst t
@@ -236,11 +255,13 @@
 
 -- | This function applies a given stateful term homomorphism with
 -- a state space propagated by the given DUTA to a term.
+          
 runUpHom :: (Functor f, Functor g) => UpState f q -> QHom f q g -> Term f -> Term g
 runUpHom st hom = snd . runUpHomSt st hom
 
 -- | This is a variant of 'runUpHom' that also returns the final state
 -- of the run.
+
 runUpHomSt :: (Functor f, Functor g) => UpState f q -> QHom f q g -> Term f -> (q,Term g)
 runUpHomSt alg h = runUpTransSt (upTrans alg h)
 
@@ -248,22 +269,27 @@
 -- | This type represents transition functions of generalised
 -- deterministic bottom-up tree acceptors (GDUTAs) which have access
 -- to an extended state space.
+
 type DUpState f p q = forall a . (?below :: a -> p, ?above :: p, q :< p) => f a -> q
 
 -- | This combinator turns an arbitrary DUTA into a GDUTA.
+
 dUpState :: Functor f => UpState f q -> DUpState f p q
 dUpState f = f . fmap below
 
 -- | This combinator turns a GDUTA with the smallest possible state
 -- space into a DUTA.
+
 upState :: DUpState f q q -> UpState f q
 upState f s = res where res = explicit f res id s
 
 -- | This combinator runs a GDUTA on a term.
+                        
 runDUpState :: Functor f => DUpState f q q -> Term f -> q
 runDUpState = runUpState . upState
 
 -- | This combinator constructs the product of two GDUTA.
+
 prodDUpState :: (p :< c, q :< c)
              => DUpState f c p -> DUpState f c q -> DUpState f c (p,q)
 prodDUpState sp sq t = (sp t, sq t)
@@ -280,39 +306,46 @@
 type DownTrans f q g = forall a. (q, f a) -> Context g (q,a)
 
 -- | Thsis function runs the given DDTT on the given tree.
+
 runDownTrans :: (Functor f, Functor g) => DownTrans f q g -> q -> Cxt h f a -> Cxt h g a
 runDownTrans tr q t = run (q,t) where
     run (q,Term t) = appCxt $ fmap run $  tr (q, t)
     run (_,Hole a)      = Hole a
 
 -- | This function runs the given DDTT on the given tree.
+    
 runDownTrans' :: (Functor f, Functor g) => DownTrans f q g -> q -> Cxt h f a -> Cxt h g (q,a)
 runDownTrans' tr q t = run (q,t) where
     run (q,Term t) = appCxt $ fmap run $  tr (q, t)
     run (q,Hole a)      = Hole (q,a)
 
--- | This function composes two DDTTs. (see Z. Fülöp, H. Vogler
--- "Syntax-Directed Semantics", Theorem 3.39)
+-- | This function composes two DDTTs. (see Z. Fulop, H. Vogler
+-- /Syntax-Directed Semantics/, Theorem 3.39)
+    
 compDownTrans :: (Functor f, Functor g, Functor h)
               => DownTrans g p h -> DownTrans f q g -> DownTrans f (q,p) h
 compDownTrans t2 t1 ((q,p), t) = fmap (\(p, (q, a)) -> ((q,p),a)) $ runDownTrans' t2 p (t1 (q, t))
 
 
 -- | This function composes a signature function after a DDTT.
+
 compSigDownTrans :: (Functor g) => SigFun g h -> DownTrans f q g -> DownTrans f q h
 compSigDownTrans sig trans = appSigFun sig . trans
 
 -- | This function composes a DDTT after a function.
+
 compDownTransSig :: DownTrans g q h -> SigFun f g -> DownTrans f q h
 compDownTransSig trans hom (q,t) = trans (q, hom t)
 
 
 -- | This function composes a homomorphism after a DDTT.
+
 compHomDownTrans :: (Functor g, Functor h)
               => Hom g h -> DownTrans f q g -> DownTrans f q h
 compHomDownTrans hom trans = appHom hom . trans
 
 -- | This function composes a DDTT after a homomorphism.
+
 compDownTransHom :: (Functor g, Functor h)
               => DownTrans g q h -> Hom f g -> DownTrans f q h
 compDownTransHom trans hom (q,t) = runDownTrans' trans q (hom t)
@@ -320,24 +353,29 @@
 
 -- | This type represents transition functions of deterministic
 -- top-down tree acceptors (DDTAs).
+
 type DownState f q = forall a. Ord a => (q, f a) -> Map a q
 
 
 -- | Changes the state space of the DDTA using the given isomorphism.
+
 tagDownState :: (q -> p) -> (p -> q) -> DownState f q -> DownState f p
 tagDownState i o t (q,s) = fmap i $ t (o q,s)
 
 -- | This function constructs the product DDTA of the given two DDTAs.
+
 prodDownState :: DownState f p -> DownState f q -> DownState f (p,q)
 prodDownState sp sq ((p,q),t) = prodMap p q (sp (p, t)) (sq (q, t))
 
 
 -- | This type is needed to construct the product of two DDTAs.
+
 data ProdState p q = LState p
                    | RState q
                    | BState p q
 -- | This function constructs the pointwise product of two maps each
 -- with a default value.
+
 prodMap :: (Ord i) => p -> q -> Map i p -> Map i q -> Map i (p,q)
 prodMap p q mp mq = Map.map final $ Map.unionWith combine ps qs
     where ps = Map.map LState mp
@@ -353,35 +391,42 @@
 -- | Apply the given state mapping to the given functorial value by
 -- adding the state to the corresponding index if it is in the map and
 -- otherwise adding the provided default state.
+          
 appMap :: Traversable f => (forall i . Ord i => f i -> Map i q)
                        -> q -> f b -> f (q,b)
 appMap qmap q s = fmap qfun s'
     where s' = number s
           qfun k@(Numbered (_,a)) = (Map.findWithDefault q k (qmap s') ,a)
 
--- | This function constructs a DDTT from a given stateful term-- homomorphism with the state propagated by the given DDTA.
+-- | This function constructs a DDTT from a given stateful term--
+-- homomorphism with the state propagated by the given DDTA.
+          
 downTrans :: Traversable f => DownState f q -> QHom f q g -> DownTrans f q g
 downTrans st f (q, s) = explicit f q fst (appMap (curry st q) q s)
 
 
 -- | This function applies a given stateful term homomorphism with a
 -- state space propagated by the given DDTA to a term.
+
 runDownHom :: (Traversable f, Functor g)
             => DownState f q -> QHom f q g -> q -> Term f -> Term g
 runDownHom st h = runDownTrans (downTrans st h)
 
 -- | This type represents transition functions of generalised
 -- deterministic top-down tree acceptors (GDDTAs) which have access
+
 -- to an extended state space.
 type DDownState f p q = forall i . (Ord i, ?below :: i -> p, ?above :: p, q :< p)
                                 => f i -> Map i q
 
 -- | This combinator turns an arbitrary DDTA into a GDDTA.
+
 dDownState :: DownState f q -> DDownState f p q
 dDownState f t = f (above,t)
 
 -- | This combinator turns a GDDTA with the smallest possible state
 -- space into a DDTA.
+
 downState :: DDownState f q q -> DownState f q
 downState f (q,s) = res
     where res = explicit f q bel s
@@ -390,11 +435,13 @@
 
 -- | This combinator constructs the product of two dependant top-down
 -- state transformations.
+          
 prodDDownState :: (p :< c, q :< c)
                => DDownState f c p -> DDownState f c q -> DDownState f c (p,q)
 prodDDownState sp sq t = prodMap above above (sp t) (sq t)
 
 -- | This is a synonym for 'prodDDownState'.
+
 (>*<) :: (p :< c, q :< c, Functor f)
          => DDownState f c p -> DDownState f c q -> DDownState f c (p,q)
 (>*<) = prodDDownState
@@ -403,6 +450,7 @@
 -- | This combinator combines a bottom-up and a top-down state
 -- transformations. Both state transformations can depend mutually
 -- recursive on each other.
+
 runDState :: Traversable f => DUpState f (u,d) u -> DDownState f (u,d) d -> d -> Term f -> u
 runDState up down d (Term t) = u where
         t' = fmap bel $ number t
@@ -415,6 +463,7 @@
 -- | This combinator runs a stateful term homomorphisms with a state
 -- space produced both on a bottom-up and a top-down state
 -- transformation.
+        
 runQHom :: (Traversable f, Functor g) =>
            DUpState f (u,d) u -> DDownState f (u,d) d -> 
            QHom f (u,d) g ->
diff --git a/src/Data/Comp/Multi/Algebra.hs b/src/Data/Comp/Multi/Algebra.hs
--- a/src/Data/Comp/Multi/Algebra.hs
+++ b/src/Data/Comp/Multi/Algebra.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE GADTs, RankNTypes, TypeOperators, ScopedTypeVariables, 
+{-# LANGUAGE GADTs, Rank2Types, TypeOperators, ScopedTypeVariables, 
   FlexibleContexts, KindSignatures #-}
 --------------------------------------------------------------------------------
 -- |
diff --git a/src/Data/Comp/Multi/Annotation.hs b/src/Data/Comp/Multi/Annotation.hs
--- a/src/Data/Comp/Multi/Annotation.hs
+++ b/src/Data/Comp/Multi/Annotation.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE TypeOperators, MultiParamTypeClasses,
-  FlexibleInstances, UndecidableInstances, RankNTypes, GADTs, ScopedTypeVariables #-}
+  FlexibleInstances, UndecidableInstances, Rank2Types, GADTs, ScopedTypeVariables #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Multi.Annotation
diff --git a/src/Data/Comp/Multi/Generic.hs b/src/Data/Comp/Multi/Generic.hs
--- a/src/Data/Comp/Multi/Generic.hs
+++ b/src/Data/Comp/Multi/Generic.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE GADTs, ExistentialQuantification, TypeOperators, ScopedTypeVariables, RankNTypes #-}
+{-# LANGUAGE GADTs, ExistentialQuantification, TypeOperators, ScopedTypeVariables, Rank2Types #-}
 
 --------------------------------------------------------------------------------
 -- |
diff --git a/src/Data/Comp/Multi/HFoldable.hs b/src/Data/Comp/Multi/HFoldable.hs
--- a/src/Data/Comp/Multi/HFoldable.hs
+++ b/src/Data/Comp/Multi/HFoldable.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE RankNTypes, TypeOperators, FlexibleInstances, ScopedTypeVariables, GADTs, MultiParamTypeClasses, UndecidableInstances, IncoherentInstances #-}
+{-# LANGUAGE Rank2Types, TypeOperators, FlexibleInstances, ScopedTypeVariables, GADTs, MultiParamTypeClasses, UndecidableInstances, IncoherentInstances #-}
 
 --------------------------------------------------------------------------------
 -- |
diff --git a/src/Data/Comp/Multi/HFunctor.hs b/src/Data/Comp/Multi/HFunctor.hs
--- a/src/Data/Comp/Multi/HFunctor.hs
+++ b/src/Data/Comp/Multi/HFunctor.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE RankNTypes, TypeOperators, FlexibleInstances, ScopedTypeVariables, GADTs, MultiParamTypeClasses, UndecidableInstances, IncoherentInstances #-}
+{-# LANGUAGE Rank2Types, TypeOperators, FlexibleInstances, ScopedTypeVariables, GADTs, MultiParamTypeClasses, UndecidableInstances, IncoherentInstances #-}
 
 --------------------------------------------------------------------------------
 -- |
diff --git a/src/Data/Comp/Multi/HTraversable.hs b/src/Data/Comp/Multi/HTraversable.hs
--- a/src/Data/Comp/Multi/HTraversable.hs
+++ b/src/Data/Comp/Multi/HTraversable.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE RankNTypes, TypeOperators, FlexibleInstances, ScopedTypeVariables, GADTs, MultiParamTypeClasses, UndecidableInstances, IncoherentInstances #-}
+{-# LANGUAGE Rank2Types, TypeOperators, FlexibleInstances, ScopedTypeVariables, GADTs, MultiParamTypeClasses, UndecidableInstances, IncoherentInstances #-}
 
 --------------------------------------------------------------------------------
 -- |
diff --git a/src/Data/Comp/Multi/Show.hs b/src/Data/Comp/Multi/Show.hs
--- a/src/Data/Comp/Multi/Show.hs
+++ b/src/Data/Comp/Multi/Show.hs
@@ -29,6 +29,9 @@
 instance KShow (K String) where
     kshow = id
 
+instance KShow (K ()) where
+    kshow _ = K $ show ()
+
 instance (ShowHF f, HFunctor f) => ShowHF (Cxt h f) where
     showHF (Hole s) = s
     showHF (Term t) = showHF $ hfmap showHF t
diff --git a/src/Data/Comp/Multi/Sum.hs b/src/Data/Comp/Multi/Sum.hs
--- a/src/Data/Comp/Multi/Sum.hs
+++ b/src/Data/Comp/Multi/Sum.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE TypeOperators, GADTs, ScopedTypeVariables, IncoherentInstances,
-  RankNTypes, FlexibleContexts, TemplateHaskell #-}
+  Rank2Types, FlexibleContexts, TemplateHaskell #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Multi.Sum
diff --git a/src/Data/Comp/Multi/Term.hs b/src/Data/Comp/Multi/Term.hs
--- a/src/Data/Comp/Multi/Term.hs
+++ b/src/Data/Comp/Multi/Term.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE EmptyDataDecls, GADTs, KindSignatures, RankNTypes,
+{-# LANGUAGE EmptyDataDecls, GADTs, KindSignatures, Rank2Types,
   TypeOperators, ScopedTypeVariables, IncoherentInstances #-}
 --------------------------------------------------------------------------------
 -- |
diff --git a/src/Data/Comp/Multi/Variables.hs b/src/Data/Comp/Multi/Variables.hs
--- a/src/Data/Comp/Multi/Variables.hs
+++ b/src/Data/Comp/Multi/Variables.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE MultiParamTypeClasses, GADTs, FlexibleInstances,
-  OverlappingInstances, TypeOperators, KindSignatures, FlexibleContexts, ScopedTypeVariables, RankNTypes, TemplateHaskell #-}
+  OverlappingInstances, TypeOperators, KindSignatures, FlexibleContexts, ScopedTypeVariables, Rank2Types, TemplateHaskell #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Multi.Variables
@@ -26,7 +26,6 @@
      variables,
      variableList,
      variables',
-     substVars,
      appSubst,
      compSubst
     ) where
@@ -41,10 +40,6 @@
 import Data.Maybe
 
 
--- type CxtSubst h a f v =  [A (v :*: (Cxt h f a))]
-
--- type Subst f v = CxtSubst NoHole Nothing f v
-
 type GSubst v a = NatM Maybe (K v) a
 
 type CxtSubst h a f v =  GSubst v (Cxt h f a)
@@ -59,6 +54,15 @@
     isVar _ = Nothing
     bindsVars :: f a :=> [v]
     bindsVars _ = []
+    
+-- | Same as 'isVar' but it returns Nothing@ instead of @Just v@ if
+-- @v@ is contained in the given set of variables.
+    
+isVar' :: (HasVars f v, Ord v) => Set v -> f a :=> Maybe v
+isVar' b t = do v <- isVar t
+                if v `Set.member` b
+                   then Nothing
+                   else return v
 
 $(derive [liftSum] [''HasVars])
 
@@ -133,31 +137,22 @@
 {-| This function substitutes variables in a context according to a
 partial mapping from variables to contexts.-}
 class SubstVars v t a where
-    substVars :: GSubst v t -> a :-> a
+    substVars :: (Set v) -> GSubst v t -> a :-> a
 
 appSubst :: SubstVars v t a => GSubst v t -> a :-> a
-appSubst = substVars
+appSubst = substVars Set.empty
 
 instance (Ord v, HasVars f v, HFunctor f) => SubstVars v (Cxt h f a) (Cxt h f a) where
     -- have to use explicit GADT pattern matching!!
-    -- subst f = free (substAlg f) Hole
-    substVars _ (Hole a) = Hole a
-    substVars f (Term v) = substAlg f v
+    substVars _ _ (Hole a) = Hole a
+    substVars b f (Term v) = substAlg f (hfmap (substVars newBound f) v)
         where  substAlg :: (HasVars f v) => CxtSubst h a f v
                         -> Alg f (Cxt h f a)
-               substAlg f t = fromMaybe (Term t) (isVar t >>= f . K)
-    -- The code below does not work with GHC 7
-    -- substVars _ (Hole a) = Hole a
-    -- substVars f (Term v) = let f' = res (bindsVars v) f in
-    --                         substAlg f' $ hfmap (substVars f') v
-    --     where  substAlg :: (HasVars f v) => CxtSubst h a f v
-    --                     -> Alg f (Cxt h f a)
-    --            substAlg f t = fromMaybe (Term t) (isVar t >>= f . K)
-    --            res :: Eq v => [v] -> GSubst v t -> GSubst v t
-    --            res vars f x = if unK x `elem` vars then Nothing else f x
+               substAlg f t = fromMaybe (Term t) (isVar' b t >>= f . K)
+               newBound = b `Set.union` Set.fromList (bindsVars v)
 
 instance (SubstVars v t a, HFunctor f) => SubstVars v t (f a) where
-    substVars f = hfmap (substVars f) 
+    substVars b f = hfmap (substVars b f) 
 
 {-| This function composes two substitutions @s1@ and @s2@. That is,
 applying the resulting substitution is equivalent to first applying
diff --git a/src/Data/Comp/MultiParam/Algebra.hs b/src/Data/Comp/MultiParam/Algebra.hs
--- a/src/Data/Comp/MultiParam/Algebra.hs
+++ b/src/Data/Comp/MultiParam/Algebra.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables, TypeOperators,
+{-# LANGUAGE GADTs, Rank2Types, ScopedTypeVariables, TypeOperators,
   FlexibleContexts, CPP, KindSignatures #-}
 --------------------------------------------------------------------------------
 -- |
diff --git a/src/Data/Comp/MultiParam/Annotation.hs b/src/Data/Comp/MultiParam/Annotation.hs
--- a/src/Data/Comp/MultiParam/Annotation.hs
+++ b/src/Data/Comp/MultiParam/Annotation.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances,
-  UndecidableInstances, RankNTypes, GADTs, ScopedTypeVariables #-}
+  UndecidableInstances, Rank2Types, GADTs, ScopedTypeVariables #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.MultiParam.Annotation
diff --git a/src/Data/Comp/MultiParam/HDifunctor.hs b/src/Data/Comp/MultiParam/HDifunctor.hs
--- a/src/Data/Comp/MultiParam/HDifunctor.hs
+++ b/src/Data/Comp/MultiParam/HDifunctor.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, RankNTypes,
+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, Rank2Types,
   TypeOperators, GADTs #-}
 --------------------------------------------------------------------------------
 -- |
diff --git a/src/Data/Comp/MultiParam/HDitraversable.hs b/src/Data/Comp/MultiParam/HDitraversable.hs
--- a/src/Data/Comp/MultiParam/HDitraversable.hs
+++ b/src/Data/Comp/MultiParam/HDitraversable.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE RankNTypes, FlexibleInstances, MultiParamTypeClasses,
+{-# LANGUAGE Rank2Types, FlexibleInstances, MultiParamTypeClasses,
   FlexibleContexts, OverlappingInstances, TypeOperators, GADTs #-}
 --------------------------------------------------------------------------------
 -- |
diff --git a/src/Data/Comp/Param/Algebra.hs b/src/Data/Comp/Param/Algebra.hs
--- a/src/Data/Comp/Param/Algebra.hs
+++ b/src/Data/Comp/Param/Algebra.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE GADTs, RankNTypes, ScopedTypeVariables, TypeOperators,
+{-# LANGUAGE GADTs, Rank2Types, ScopedTypeVariables, TypeOperators,
   FlexibleContexts, CPP #-}
 --------------------------------------------------------------------------------
 -- |
diff --git a/src/Data/Comp/Param/Annotation.hs b/src/Data/Comp/Param/Annotation.hs
--- a/src/Data/Comp/Param/Annotation.hs
+++ b/src/Data/Comp/Param/Annotation.hs
@@ -1,5 +1,5 @@
 {-# LANGUAGE TypeOperators, MultiParamTypeClasses, FlexibleInstances,
-  UndecidableInstances, RankNTypes, GADTs, ScopedTypeVariables #-}
+  UndecidableInstances, Rank2Types, GADTs, ScopedTypeVariables #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Param.Annotation
diff --git a/src/Data/Comp/Param/Thunk.hs b/src/Data/Comp/Param/Thunk.hs
--- a/src/Data/Comp/Param/Thunk.hs
+++ b/src/Data/Comp/Param/Thunk.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, FlexibleContexts, RankNTypes, GADTs #-}
+{-# LANGUAGE TypeOperators, FlexibleContexts, Rank2Types, GADTs #-}
 
 --------------------------------------------------------------------------------
 -- |
diff --git a/src/Data/Comp/Term.hs b/src/Data/Comp/Term.hs
--- a/src/Data/Comp/Term.hs
+++ b/src/Data/Comp/Term.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE EmptyDataDecls, GADTs, KindSignatures, RankNTypes #-}
+{-# LANGUAGE EmptyDataDecls, GADTs, KindSignatures, Rank2Types #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.Term
diff --git a/src/Data/Comp/TermRewriting.hs b/src/Data/Comp/TermRewriting.hs
--- a/src/Data/Comp/TermRewriting.hs
+++ b/src/Data/Comp/TermRewriting.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE RankNTypes, GADTs #-}
+{-# LANGUAGE Rank2Types, GADTs #-}
 --------------------------------------------------------------------------------
 -- |
 -- Module      :  Data.Comp.TermRewriting
diff --git a/src/Data/Comp/Thunk.hs b/src/Data/Comp/Thunk.hs
--- a/src/Data/Comp/Thunk.hs
+++ b/src/Data/Comp/Thunk.hs
@@ -1,4 +1,4 @@
-{-# LANGUAGE TypeOperators, FlexibleContexts, RankNTypes, ScopedTypeVariables #-}
+{-# LANGUAGE TypeOperators, FlexibleContexts, Rank2Types, ScopedTypeVariables #-}
 
 --------------------------------------------------------------------------------
 -- |