diff --git a/CHANGES b/CHANGES
new file mode 100644
--- /dev/null
+++ b/CHANGES
@@ -0,0 +1,21 @@
+Version 0.2: 24 March 2011
+
+  * Initial release to go along with submission of "Binders Unbound".
+
+Version 0.2.1: 28 March 2011
+
+  * Massive update to documentation.
+
+Version 0.2.2: 29 March 2011
+
+  * Add MonadFix instances for FreshM and LFreshM.  Thanks to Job
+    Vranish for the suggestion.
+
+Version 0.2.3: 20 April 2011
+
+  * Fix minor bugs in
+    - tutorial/Tutorial.lhs
+    - examples/Abstract.hs
+    - examples/STLC.hs
+
+    Thanks to Ki Yung Ahn for the reports.
diff --git a/examples/Abstract.hs b/examples/Abstract.hs
new file mode 100644
--- /dev/null
+++ b/examples/Abstract.hs
@@ -0,0 +1,176 @@
+{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,
+    TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,
+    ScopedTypeVariables, MultiParamTypeClasses, StandaloneDeriving
+ #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  LC
+-- Copyright   :  (c) The University of Pennsylvania, 2010
+-- License     :  BSD
+--
+-- Maintainer  :  sweirich@cis.upenn.edu
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+--
+--
+-----------------------------------------------------------------------------
+
+-- | This example demonstrates how to use abstract types as part of
+-- the syntax of the untyped lambda calculus
+--
+-- Suppose we wish to include Source positions in our Abstract Syntax
+--
+module Abstract where
+
+import Generics.RepLib
+import Unbound.LocallyNameless
+
+import qualified Data.Set as S
+
+
+-- We import the type SourcePos, but it is an abstract data type
+-- all we know about it is that it is an instance of the Eq, Show and Ord classes.
+import Text.ParserCombinators.Parsec.Pos (SourcePos, newPos)
+
+-- Since we don't know the structure of the type, we create an "abstract"
+-- representation for it. This defines rSourcePos :: R SourcePos and makes
+-- SourcePos an instance of the Rep and Rep1 type classes.
+--
+-- Right now, this line triggers a warning because the TemplateHaskell code
+-- does not work well with type abbreviations. The warning is safe to ignore.
+$(derive_abstract [''SourcePos])
+
+-- | A Simple datatype for the Lambda Calculus that includes source position
+-- information
+data Exp = Var SourcePos (Name Exp)
+         | Lam (Bind (Name Exp) Exp)
+         | App Exp Exp
+  deriving Show
+
+$(derive [''Exp])
+
+-- To make Exp an instance of Alpha, we also need SourcePos to be an
+-- instance of Alpha, because it appears inside the Exp type.  When we
+-- do so, we override the default definition of aeq'.  There are a
+-- few reasonable choices for this:
+--
+-- (1) match no source positions together  --- default definition
+--      aeq' c s1 s2 = False
+-- (2) match all source positions together
+--      aeq' c s1 s2 = True
+-- (3) only match equal source positions together
+--      aeq' c s1 s2 = s1 == s2
+--
+--
+-- Below, we choose option (2) because we would like
+-- (alpha-)equivalence for Exp to ignore the source position
+-- information. Two free variables with the same name but with
+-- different source positions should be equal.
+--
+-- The other defaults for Alpha are fine.
+instance Alpha SourcePos where
+   aeq' c s1 s2 = True
+   acompare' c s1 s2 = EQ
+
+instance Alpha Exp where
+
+instance Subst Exp SourcePos where
+instance Subst Exp Exp where
+   isvar (Var _ x) = Just (SubstName x)
+   isvar _       = Nothing
+
+type M a = LFreshM a
+
+-- | Beta-Eta equivalence for lambda calculus terms.
+(=~) :: Exp -> Exp -> M Bool
+e1 =~ e2 | e1 `aeq` e2 = return True
+e1 =~ e2 = do
+    e1' <- red e1
+    e2' <- red e2
+    if e1' `aeq` e1 && e2' `aeq` e2
+      then return False
+      else e1' =~ e2'
+
+
+-- | Parallel beta-eta reduction for lambda calculus terms.
+-- Do as many reductions as possible in one step, while still ensuring
+-- termination.
+red :: Exp -> M Exp
+red (App e1 e2) = do
+  e1' <- red e1
+  e2' <- red e2
+  case e1' of
+    -- look for a beta-reduction
+    Lam bnd ->
+      lunbind bnd $ \ (x, e1'') ->
+        return $ subst x e2' e1''
+    otherwise -> return $ App e1' e2'
+red (Lam bnd) = lunbind bnd $ \ (x, e) -> do
+   e' <- red e
+   case e of
+     -- look for an eta-reduction
+     App e1 (Var _ y) | y `aeq` x && x `S.notMember` fv e1 -> return e1
+     otherwise -> return (Lam (bind x e'))
+red v = return $ v
+
+
+
+---------------------------------------------------------------------
+-- Some testing code to demonstrate this library in action.
+
+assert :: String -> Bool -> IO ()
+assert s True  = return ()
+assert s False = print ("Assertion " ++ s ++ " failed")
+
+assertM :: String -> M Bool -> IO ()
+assertM s c =
+  if (runLFreshM c) then return ()
+  else print ("Assertion " ++ s ++ " failed")
+
+x :: Name Exp
+x = string2Name "x"
+
+y :: Name Exp
+y = string2Name "y"
+
+z :: Name Exp
+z = string2Name "z"
+
+s :: Name Exp
+s = string2Name "s"
+
+sp = newPos "Foo" 1 2
+sp2 = newPos "Bar" 3 4
+
+lam :: Name Exp -> Exp -> Exp
+lam x y = Lam (bind x y)
+
+var :: Name Exp -> Exp
+var n = Var sp n
+
+zero  = lam s (lam z (var z))
+one   = lam s (lam z (App (var s) (var z)))
+two   = lam s (lam z (App (var s) (App (var s) (var z))))
+three = lam s (lam z (App (var s) (App (var s) (App (var s) (var z)))))
+
+plus = lam x (lam y (lam s (lam z (App (App (var x) (var s)) (App (App (var y) (var s)) (var z))))))
+
+true = lam x (lam y (var x))
+false = lam x (lam y (var y))
+if_ x y z = (App (App x y) z)
+
+main :: IO ()
+main = do
+  -- \x.x `aeq` \x.y, no matter what the source positions are
+  assert "a1" $ lam x (var x) `aeq` lam y (Var sp2 y)
+  -- \x.x /= \x.y
+  assert "a2" $ not(lam x (var y) `aeq` lam x (var x))
+  -- \x.(\y.x) (\y.y) `aeq` \y.y
+  assertM "be1" $ lam x (App (lam y (var x)) (lam y (var y))) =~ (lam y (var y))
+  -- \x. f x `aeq` f
+  assertM "be2" $ lam x (App (var y) (var x)) =~ var y
+  assertM "be3" $ if_ true (var x) (var y) =~ var x
+  assertM "be4" $ if_ false (var x) (var y) =~ var y
+  assertM "be5" $ App (App plus one) two =~ three
+
diff --git a/examples/Functor.hs b/examples/Functor.hs
new file mode 100644
--- /dev/null
+++ b/examples/Functor.hs
@@ -0,0 +1,110 @@
+{-# LANGUAGE TemplateHaskell,
+             ScopedTypeVariables,
+             FlexibleInstances,
+             MultiParamTypeClasses,
+             FlexibleContexts,
+             UndecidableInstances,
+             GADTs #-}
+
+module Functor where
+
+import Unbound.LocallyNameless hiding (Int)
+import Control.Monad
+import Control.Monad.Trans.Error
+import Data.List as List
+
+{- So we can't actually do modules like I was thinking of.
+   Substitution in modules only "delays" capture not avoids it.
+ -}
+
+type TyName = Name Type
+type ModName = Name Module
+
+data Type = TyVar TyName
+          | Int
+          | Bool
+          | Path Module TyName
+   deriving Show
+
+data ModDef =  TyDef TyName (Maybe (Embed Type))
+            |  ModDef ModName Module
+                 -- here is the question. For submodules should
+                 -- it be Embed Module or just Module?  For the
+                 -- former, then the "binding" names of the submodule
+                 -- could be bound by the outer module. For the latter
+                 -- a submodule can't use the same name as the outer
+                 -- module.
+   deriving Show
+data Module =  Struct  (Rec [ModDef])
+            |  Functor (Bind TyName Module)
+            |  ModApp Module Type
+            |  ModVar (Name Module)
+   deriving Show
+
+$(derive [''Type, ''ModDef, ''Module])
+
+------------------------------------------------------
+instance Alpha Type where
+instance Alpha Module where
+instance Alpha ModDef where
+
+instance Subst Module Type where
+
+instance Subst Module ModDef
+instance Subst Module Module where
+  isvar (ModVar x) = Just (SubstName x)
+  isvar _ = Nothing
+
+instance Subst Type Module where
+instance Subst Type ModDef where
+instance Subst Type Type where
+  isvar (TyVar x) = Just (SubstName x)
+  isvar _ = Nothing
+
+t :: TyName
+t = string2Name "t"
+
+u :: TyName
+u = string2Name "u"
+
+x :: TyName
+x = string2Name "x"
+
+g :: ModName
+g = string2Name "G"
+
+f :: Module
+f = Functor (bind x
+             (Struct (rec [TyDef t (Just (Embed Bool)),
+             TyDef u (Just (Embed (TyVar x)))])))
+
+m :: Module
+m = Struct (rec [TyDef t (Just (Embed Int)),
+                 ModDef g (ModApp f (TyVar t))])
+
+
+red :: Fresh m => Module -> m Module
+red (ModApp m1 t) = do
+  m1' <- red m1
+  case m1' of
+    Functor bnd -> do
+       (x, m1'') <- unbind bnd
+       red (subst x t m1'')
+    _ -> return (ModApp m1 t)
+red (Struct s) = do
+    defs <- mapM redDef (unrec s)
+    return (Struct (rec defs))
+red m = return m
+
+redDef :: Fresh m => ModDef -> m ModDef
+redDef (ModDef f m) = do
+  m' <- red m
+  return (ModDef f m')
+redDef d = return d
+
+m3 = Struct (rec [TyDef t Nothing,
+                  TyDef u (Just (Embed (TyVar t)))])
+
+m2 :: Module
+m2 = runFreshM (red m)
+
diff --git a/examples/Functor2.hs b/examples/Functor2.hs
new file mode 100644
--- /dev/null
+++ b/examples/Functor2.hs
@@ -0,0 +1,104 @@
+{-# LANGUAGE TemplateHaskell,
+             ScopedTypeVariables,
+             FlexibleInstances,
+             MultiParamTypeClasses,
+             FlexibleContexts,
+             UndecidableInstances,
+             GADTs #-}
+
+module Functor2 where
+
+import Unbound.LocallyNameless hiding (Int)
+import Control.Monad
+import Control.Monad.Trans.Error
+import Data.List as List
+
+{- This is the right way to formalize modules and functors
+ -}
+
+type TyName = Name Type
+type ModName = Name Module
+
+data Type = TyVar TyName
+          | Int
+          | Bool
+          | Path Module String
+   deriving Show
+
+data ModDef =  TyDef  TyName  (Maybe (Embed Type))
+            |  ModDef ModName (Embed Module)
+
+   deriving Show
+data Module =  Struct  (Bind (Rec [(String,ModDef)]) ())
+            |  Functor (Bind TyName Module)
+            |  ModApp Module Type
+            |  ModVar (Name Module)
+   deriving Show
+
+$(derive [''Type, ''ModDef, ''Module])
+
+------------------------------------------------------
+instance Alpha Type where
+instance Alpha Module where
+instance Alpha ModDef where
+
+instance Subst Module Type where
+
+instance Subst Module ModDef
+instance Subst Module Module where
+  isvar (ModVar x) = Just (SubstName x)
+  isvar _ = Nothing
+
+instance Subst Type Module where
+instance Subst Type ModDef where
+instance Subst Type Type where
+  isvar (TyVar x) = Just (SubstName x)
+  isvar _ = Nothing
+
+
+t :: TyName
+t = string2Name "t"
+
+u :: TyName
+u = string2Name "u"
+
+x :: TyName
+x = string2Name "x"
+
+g :: ModName
+g = string2Name "G"
+
+f :: Module
+f = Functor (bind x
+             (Struct (bind (rec
+                  [("t", TyDef t (Just (Embed Bool))),
+                   ("u", TyDef u (Just (Embed (TyVar x))))]) ())))
+
+m :: Module
+m = Struct (bind (rec [("t", TyDef t (Just (Embed Int))),
+                       ("g", ModDef g (Embed (ModApp f (TyVar t))))]) ())
+
+
+red :: Fresh m => Module -> m Module
+red (ModApp m1 t) = do
+  m1' <- red m1
+  case m1' of
+    Functor bnd -> do
+       (x, m1'') <- unbind bnd
+       red (subst x t m1'')
+    _ -> return (ModApp m1 t)
+red (Struct s) = do
+    (r,()) <- unbind s
+    defs <- mapM redDef (unrec r)
+    return (Struct (bind (rec defs) ()))
+red m = return m
+
+redDef :: Fresh m => (String,ModDef) -> m (String,ModDef)
+redDef (s,ModDef f (Embed m)) = do
+  m' <- red m
+  return (s,ModDef f (Embed m'))
+redDef d = return d
+
+m2 :: Module
+m2 = runFreshM (red m)
+
diff --git a/examples/Issue15.hs b/examples/Issue15.hs
new file mode 100644
--- /dev/null
+++ b/examples/Issue15.hs
@@ -0,0 +1,13 @@
+{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,
+    TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,
+    ScopedTypeVariables, MultiParamTypeClasses, StandaloneDeriving
+ #-}
+
+module Issue15 where
+
+import Generics.RepLib
+import qualified Unbound.LocallyNameless as LN
+
+data Foo = Foo (LN.Name Foo)
+
+$(derive [''Foo])
diff --git a/examples/STLC.hs b/examples/STLC.hs
--- a/examples/STLC.hs
+++ b/examples/STLC.hs
@@ -19,7 +19,6 @@
 module STLC where
 
 import Unbound.LocallyNameless
-import Control.Monad.Reader
 import Data.Set as S
 
 data Ty = TInt | TUnit | Arr Ty Ty
@@ -47,8 +46,7 @@
 
 type Ctx = [(Name Exp, Ty)]
 
--- A monad that can generate locally fresh names
-type M a = Reader Integer a
+type M a = LFreshM a
 
 -- A type checker for STLC terms
 tc :: Ctx -> Exp -> Ty -> M Bool
@@ -165,7 +163,7 @@
 
 assertM :: (a -> Bool) -> String -> M a -> IO ()
 assertM f s c =
-  if f (runReader c (0 :: Integer)) then return ()
+  if f (runLFreshM c) then return ()
   else print ("Assertion " ++ s ++ " failed")
 
 name1, name2 :: Name Exp
diff --git a/examples/abstract.hs b/examples/abstract.hs
deleted file mode 100644
--- a/examples/abstract.hs
+++ /dev/null
@@ -1,178 +0,0 @@
-{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,
-    TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,
-    ScopedTypeVariables, MultiParamTypeClasses, StandaloneDeriving
- #-}
------------------------------------------------------------------------------
--- |
--- Module      :  LC
--- Copyright   :  (c) The University of Pennsylvania, 2010
--- License     :  BSD
---
--- Maintainer  :  sweirich@cis.upenn.edu
--- Stability   :  experimental
--- Portability :  non-portable
---
---
---
------------------------------------------------------------------------------
-
--- | This example demonstrates how to use abstract types as part of
--- the syntax of the untyped lambda calculus
---
--- Suppose we wish to include Source positions in our Abstract Syntax
---
-module Abstract where
-
-import Generics.RepLib
-import Unbound.LocallyNameless
-
-import qualified Data.Set as S
-
-import Control.Monad.Reader (Reader, runReader)
-
-
--- We import the type SourcePos, but it is an abstract data type
--- all we know about it is that it is an instance of the Eq, Show and Ord classes.
-import Text.ParserCombinators.Parsec.Pos (SourcePos, newPos)
-
--- Since we don't know the structure of the type, we create an "abstract"
--- representation for it. This defines rSourcePos :: R SourcePos and makes
--- SourcePos an instance of the Rep and Rep1 type classes.
---
--- Right now, this line triggers a warning because the TemplateHaskell code
--- does not work well with type abbreviations. The warning is safe to ignore.
-$(derive_abstract [''SourcePos])
-
--- | A Simple datatype for the Lambda Calculus that includes source position
--- information
-data Exp = Var SourcePos (Name Exp)
-         | Lam (Bind (Name Exp) Exp)
-         | App Exp Exp
-  deriving Show
-
-$(derive [''Exp])
-
--- To make Exp an instance of Alpha, we also need SourcePos to be an
--- instance of Alpha, because it appears inside the Exp type.  When we
--- do so, we override the default definition of aeq'.  There are a
--- few reasonable choices for this:
---
--- (1) match no source positions together  --- default definition
---      aeq' c s1 s2 = False
--- (2) match all source positions together
---      aeq' c s1 s2 = True
--- (3) only match equal source positions together
---      aeq' c s1 s2 = s1 == s2
---
---
--- Below, we choose option (2) because we would like
--- (alpha-)equivalence for Exp to ignore the source position
--- information. Two free variables with the same name but with
--- different source positions should be equal.
---
--- The other defaults for Alpha are fine.
-instance Alpha SourcePos where
-   aeq' c s1 s2 = True
-   acompare' c s1 s2 = EQ
-
-instance Alpha Exp where
-
-instance Subst Exp SourcePos where
-instance Subst Exp Exp where
-   isvar (Var _ x) = Just (SubstName x)
-   isvar _       = Nothing
-
-type M a = Reader Integer a
-
--- | Beta-Eta equivalence for lambda calculus terms.
-(=~) :: Exp -> Exp -> M Bool
-e1 =~ e2 | e1 `aeq` e2 = return True
-e1 =~ e2 = do
-    e1' <- red e1
-    e2' <- red e2
-    if e1' `aeq` e1 && e2' `aeq` e2
-      then return False
-      else e1' =~ e2'
-
-
--- | Parallel beta-eta reduction for lambda calculus terms.
--- Do as many reductions as possible in one step, while still ensuring
--- termination.
-red :: Exp -> M Exp
-red (App e1 e2) = do
-  e1' <- red e1
-  e2' <- red e2
-  case e1' of
-    -- look for a beta-reduction
-    Lam bnd ->
-      lunbind bnd $ \ (x, e1'') ->
-        return $ subst x e2' e1''
-    otherwise -> return $ App e1' e2'
-red (Lam bnd) = lunbind bnd $ \ (x, e) -> do
-   e' <- red e
-   case e of
-     -- look for an eta-reduction
-     App e1 (Var _ y) | y `aeq` x && x `S.notMember` fv e1 -> return e1
-     otherwise -> return (Lam (bind x e'))
-red v = return $ v
-
-
-
----------------------------------------------------------------------
--- Some testing code to demonstrate this library in action.
-
-assert :: String -> Bool -> IO ()
-assert s True  = return ()
-assert s False = print ("Assertion " ++ s ++ " failed")
-
-assertM :: String -> M Bool -> IO ()
-assertM s c =
-  if (runReader c (0 :: Integer)) then return ()
-  else print ("Assertion " ++ s ++ " failed")
-
-x :: Name Exp
-x = string2Name "x"
-
-y :: Name Exp
-y = string2Name "y"
-
-z :: Name Exp
-z = string2Name "z"
-
-s :: Name Exp
-s = string2Name "s"
-
-sp = newPos "Foo" 1 2
-sp2 = newPos "Bar" 3 4
-
-lam :: Name Exp -> Exp -> Exp
-lam x y = Lam (bind x y)
-
-var :: Name Exp -> Exp
-var n = Var sp n
-
-zero  = lam s (lam z (var z))
-one   = lam s (lam z (App (var s) (var z)))
-two   = lam s (lam z (App (var s) (App (var s) (var z))))
-three = lam s (lam z (App (var s) (App (var s) (App (var s) (var z)))))
-
-plus = lam x (lam y (lam s (lam z (App (App (var x) (var s)) (App (App (var y) (var s)) (var z))))))
-
-true = lam x (lam y (var x))
-false = lam x (lam y (var y))
-if_ x y z = (App (App x y) z)
-
-main :: IO ()
-main = do
-  -- \x.x `aeq` \x.y, no matter what the source positions are
-  assert "a1" $ lam x (var x) `aeq` lam y (Var sp2 y)
-  -- \x.x /= \x.y
-  assert "a2" $ not(lam x (var y) `aeq` lam x (var x))
-  -- \x.(\y.x) (\y.y) `aeq` \y.y
-  assertM "be1" $ lam x (App (lam y (var x)) (lam y (var y))) =~ (lam y (var y))
-  -- \x. f x `aeq` f
-  assertM "be2" $ lam x (App (var y) (var x)) =~ var y
-  assertM "be3" $ if_ true (var x) (var y) =~ var x
-  assertM "be4" $ if_ false (var x) (var y) =~ var y
-  assertM "be5" $ App (App plus one) two =~ three
-
diff --git a/examples/functor.hs b/examples/functor.hs
deleted file mode 100644
--- a/examples/functor.hs
+++ /dev/null
@@ -1,110 +0,0 @@
-{-# LANGUAGE TemplateHaskell,
-             ScopedTypeVariables,
-             FlexibleInstances,
-             MultiParamTypeClasses,
-             FlexibleContexts,
-             UndecidableInstances,
-             GADTs #-}
-
-module Functor where
-
-import Unbound.LocallyNameless hiding (Int)
-import Control.Monad
-import Control.Monad.Trans.Error
-import Data.List as List
-
-{- So we can't actually do modules like I was thinking of.
-   Substitution in modules only "delays" capture not avoids it.
- -}
-
-type TyName = Name Type
-type ModName = Name Module
-
-data Type = TyVar TyName
-          | Int
-          | Bool
-          | Path Module TyName
-   deriving Show
-
-data ModDef =  TyDef TyName (Maybe (Embed Type))
-            |  ModDef ModName Module
-                 -- here is the question. For submodules should
-                 -- it be Embed Module or just Module?  For the
-                 -- former, then the "binding" names of the submodule
-                 -- could be bound by the outer module. For the latter
-                 -- a submodule can't use the same name as the outer
-                 -- module.
-   deriving Show
-data Module =  Struct  (Rec [ModDef])
-            |  Functor (Bind TyName Module)
-            |  ModApp Module Type
-            |  ModVar (Name Module)
-   deriving Show
-
-$(derive [''Type, ''ModDef, ''Module])
-
-------------------------------------------------------
-instance Alpha Type where
-instance Alpha Module where
-instance Alpha ModDef where
-
-instance Subst Module Type where
-
-instance Subst Module ModDef
-instance Subst Module Module where
-  isvar (ModVar x) = Just (SubstName x)
-  isvar _ = Nothing
-
-instance Subst Type Module where
-instance Subst Type ModDef where
-instance Subst Type Type where
-  isvar (TyVar x) = Just (SubstName x)
-  isvar _ = Nothing
-
-t :: TyName
-t = string2Name "t"
-
-u :: TyName
-u = string2Name "u"
-
-x :: TyName
-x = string2Name "x"
-
-g :: ModName
-g = string2Name "G"
-
-f :: Module
-f = Functor (bind x
-             (Struct (rec [TyDef t (Just (Embed Bool)),
-             TyDef u (Just (Embed (TyVar x)))])))
-
-m :: Module
-m = Struct (rec [TyDef t (Just (Embed Int)),
-                 ModDef g (ModApp f (TyVar t))])
-
-
-red :: Fresh m => Module -> m Module
-red (ModApp m1 t) = do
-  m1' <- red m1
-  case m1' of
-    Functor bnd -> do
-       (x, m1'') <- unbind bnd
-       red (subst x t m1'')
-    _ -> return (ModApp m1 t)
-red (Struct s) = do
-    defs <- mapM redDef (unrec s)
-    return (Struct (rec defs))
-red m = return m
-
-redDef :: Fresh m => ModDef -> m ModDef
-redDef (ModDef f m) = do
-  m' <- red m
-  return (ModDef f m')
-redDef d = return d
-
-m3 = Struct (rec [TyDef t Nothing,
-                  TyDef u (Just (Embed (TyVar t)))])
-
-m2 :: Module
-m2 = runFreshM (red m)
-
diff --git a/examples/functor2.hs b/examples/functor2.hs
deleted file mode 100644
--- a/examples/functor2.hs
+++ /dev/null
@@ -1,104 +0,0 @@
-{-# LANGUAGE TemplateHaskell,
-             ScopedTypeVariables,
-             FlexibleInstances,
-             MultiParamTypeClasses,
-             FlexibleContexts,
-             UndecidableInstances,
-             GADTs #-}
-
-module Functor2 where
-
-import Unbound.LocallyNameless hiding (Int)
-import Control.Monad
-import Control.Monad.Trans.Error
-import Data.List as List
-
-{- This is the right way to formalize modules and functors
- -}
-
-type TyName = Name Type
-type ModName = Name Module
-
-data Type = TyVar TyName
-          | Int
-          | Bool
-          | Path Module String
-   deriving Show
-
-data ModDef =  TyDef  TyName  (Maybe (Embed Type))
-            |  ModDef ModName (Embed Module)
-
-   deriving Show
-data Module =  Struct  (Bind (Rec [(String,ModDef)]) ())
-            |  Functor (Bind TyName Module)
-            |  ModApp Module Type
-            |  ModVar (Name Module)
-   deriving Show
-
-$(derive [''Type, ''ModDef, ''Module])
-
-------------------------------------------------------
-instance Alpha Type where
-instance Alpha Module where
-instance Alpha ModDef where
-
-instance Subst Module Type where
-
-instance Subst Module ModDef
-instance Subst Module Module where
-  isvar (ModVar x) = Just (SubstName x)
-  isvar _ = Nothing
-
-instance Subst Type Module where
-instance Subst Type ModDef where
-instance Subst Type Type where
-  isvar (TyVar x) = Just (SubstName x)
-  isvar _ = Nothing
-
-
-t :: TyName
-t = string2Name "t"
-
-u :: TyName
-u = string2Name "u"
-
-x :: TyName
-x = string2Name "x"
-
-g :: ModName
-g = string2Name "G"
-
-f :: Module
-f = Functor (bind x
-             (Struct (bind (rec
-                  [("t", TyDef t (Just (Embed Bool))),
-                   ("u", TyDef u (Just (Embed (TyVar x))))]) ())))
-
-m :: Module
-m = Struct (bind (rec [("t", TyDef t (Just (Embed Int))),
-                       ("g", ModDef g (Embed (ModApp f (TyVar t))))]) ())
-
-
-red :: Fresh m => Module -> m Module
-red (ModApp m1 t) = do
-  m1' <- red m1
-  case m1' of
-    Functor bnd -> do
-       (x, m1'') <- unbind bnd
-       red (subst x t m1'')
-    _ -> return (ModApp m1 t)
-red (Struct s) = do
-    (r,()) <- unbind s
-    defs <- mapM redDef (unrec r)
-    return (Struct (bind (rec defs) ()))
-red m = return m
-
-redDef :: Fresh m => (String,ModDef) -> m (String,ModDef)
-redDef (s,ModDef f (Embed m)) = do
-  m' <- red m
-  return (s,ModDef f (Embed m'))
-redDef d = return d
-
-m2 :: Module
-m2 = runFreshM (red m)
-
diff --git a/examples/issue15.hs b/examples/issue15.hs
deleted file mode 100644
--- a/examples/issue15.hs
+++ /dev/null
@@ -1,13 +0,0 @@
-{-# LANGUAGE TemplateHaskell, UndecidableInstances, ExistentialQuantification,
-    TypeOperators, GADTs, TypeSynonymInstances, FlexibleInstances,
-    ScopedTypeVariables, MultiParamTypeClasses, StandaloneDeriving
- #-}
-
-module Issue15 where
-
-import Generics.RepLib
-import qualified Unbound.LocallyNameless as LN
-
-data Foo = Foo (LN.Name Foo)
-
-$(derive [''Foo])
diff --git a/tutorial/Tutorial.lhs b/tutorial/Tutorial.lhs
--- a/tutorial/Tutorial.lhs
+++ b/tutorial/Tutorial.lhs
@@ -581,7 +581,7 @@
 >   checkEq b a
 > 
 > checkList :: Tele -> [Exp] -> Tele -> M ()
-> checkList _ [] Empty = ok
+> checkList _ [] Empty = return ()
 > checkList g (e:es) (Cons rb) = do
 >   let ((x, Embed a), t') = unrebind rb
 >   check g e a
diff --git a/unbound.cabal b/unbound.cabal
--- a/unbound.cabal
+++ b/unbound.cabal
@@ -1,5 +1,5 @@
 name:           unbound
-version:        0.2.2
+version:        0.2.3
 license:        BSD3
 license-file:   LICENSE
 build-type:     Simple
@@ -11,6 +11,7 @@
 homepage:       http://code.google.com/p/replib/
 category:       Language, Generics, Compilers/Interpreters
 extra-source-files: README, 
+                    CHANGES,
                     examples/*.hs,
                     tutorial/Makefile,
                     tutorial/Tutorial.lhs,