diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2008, Sebastian Fischer
+Copyright (c) 2008-2009, Sebastian Fischer
 
 All rights reserved.
 
diff --git a/README b/README
--- a/README
+++ b/README
@@ -12,6 +12,6 @@
 
 [cflp]: http://www-ps.informatik.uni-kiel.de/~sebf/projects/cflp.html
 
-Sebastian Fischer, 2008
+Sebastian Fischer,
 sebf@informatik.uni-kiel.de
 
diff --git a/cflp.cabal b/cflp.cabal
--- a/cflp.cabal
+++ b/cflp.cabal
@@ -1,5 +1,5 @@
 Name:          cflp
-Version:       2009.1.15.2
+Version:       2009.1.16
 Cabal-Version: >= 1.6
 Synopsis:      Constraint Functional-Logic Programming in Haskell
 Description:   This package provides combinators for constraint
@@ -35,12 +35,12 @@
                     Control.Constraint.Choice,
                     Data.LazyNondet,
                     Data.LazyNondet.Types,
+                    Data.LazyNondet.Generic,
                     Data.LazyNondet.UniqueID,
                     Data.LazyNondet.Matching,
                     Data.LazyNondet.Narrowing,
                     Data.LazyNondet.Primitive,
                     Data.LazyNondet.HigherOrder,
-                    Data.LazyNondet.Generic,
                     Control.CFLP.Tests,
                     Control.CFLP.Tests.CallTimeChoice
                     Control.CFLP.Tests.HigherOrder
diff --git a/src/Control/CFLP/Tests/HigherOrder.lhs b/src/Control/CFLP/Tests/HigherOrder.lhs
--- a/src/Control/CFLP/Tests/HigherOrder.lhs
+++ b/src/Control/CFLP/Tests/HigherOrder.lhs
@@ -10,7 +10,8 @@
 > import Control.CFLP.Tests
 > import Test.HUnit
 >
-> import Prelude hiding ( not, null, head, map, foldr )
+> import Prelude hiding ( not, null, head, map, foldr, flip, id )
+> import qualified Prelude as P
 > import Data.LazyNondet.Types.Bool
 > import Data.LazyNondet.Types.List
 >
@@ -22,6 +23,10 @@
 >   , "call-time choice" ~: callTimeChoice
 >   , "map shared unknowns" ~: mapSharedUnknowns
 >   , "memeber with fold" ~: memberWithFold
+>   , "overApplication" ~: overApplication
+>   , "reverse with foldr" ~: reverseWithFoldr
+>   -- , "pointfree reverse" ~: pointfreeReverse
+>   -- , "function conversion" ~: functionConversion
 >   ]
 
 The following test simply applies the not function.
@@ -75,4 +80,74 @@
 > memberWithFold = assertResults comp [True,False]
 >  where
 >   comp = foldr (fun (?)) failure (true ^: false ^: nil)
+
+The following test applies the composition function which is has a
+function on its right-hand side:
+
+> after :: CFLP cs m
+>       => Nondet cs m (b -> c) -> Nondet cs m (a -> b)
+>       -> Nondet cs m (a -> c)
+> after f g = fun (\x cs -> withUnique $ \u -> apply f (apply g x cs u) cs)
+>
+> overApplication :: Assertion
+> overApplication = assertResults comp [True]
+>  where
+>   comp = apply (after (fun not) (fun not)) true
+
+The following test makes extensive use of higher-order features by
+implementing the reverse function using `foldr`.
+
+~~~ { .Haskell }
+rev = flip (foldr (\x f l -> f (x:l)) id) []
+~~~
+
+> reverseWithFoldr :: Assertion
+> reverseWithFoldr = assertResults comp [[True,False,False]]
+>  where
+>   comp = rev (false ^: false ^: true ^: nil)
+>   rev  = flip (fun (foldr (fun (\x f l -> apply f (x ^: l))) (fun id))) nil
+>
+> flip :: CFLP cs m
+>      => Nondet cs m (a -> b -> c) -> Nondet cs m b -> Nondet cs m a
+>      -> Context cs -> ID -> Nondet cs m c
+> flip f x y cs = withUnique $ \u -> apply (apply f y cs u) x cs
+> 
+> id :: Nondet cs m a -> Nondet cs m a
+> id x = x
+
+The following uses even more higher-order functions by implementing a
+pointfree version of the above reverse function.
+
+~~~ { .Haskell }
+rev = flip (foldr (flip (flip ((.).(.)) (:))) id) []
+~~~
+
+-- > pointfreeReverse :: Assertion
+-- > pointfreeReverse = assertResults comp [[True,False,False]]
+-- >  where
+-- >   comp cs = withUnique $ \u ->
+-- >               apply (rev cs u) (false ^: false ^: true ^: nil) cs
+-- > rev cs u = fun (flip (fun (foldr (fun (flip (fun (flip ((fun after `after` fun after) cs u) (fun (^:)))))) (fun id))) nil)
+
+Currently, GHC (6.10.1) fails to compile the definition. The problem
+seems to occur with many uses of `fun`:
+
+-- > compileTimePerformanceBug
+-- >   = fun id `after` fun id
+-- >            `after` fun id
+-- >            `after` fun id
+-- >            `after` fun id
+-- >            `after` fun id
+-- >            `after` fun id
+
+The following test converts primitive Haskell functions to
+non-deterministic ones and applies them to non-deterministic values.
+
+> functionConversion :: Assertion
+> functionConversion = assertResults comp [False]
+>  where
+>   comp cs = withUnique $ \u ->
+>              apply (foldr (fun after) (fun id)
+>                       (nondet [P.not,P.not,P.not]) cs u)
+>                true cs
 
diff --git a/src/Data/LazyNondet/Generic.lhs b/src/Data/LazyNondet/Generic.lhs
--- a/src/Data/LazyNondet/Generic.lhs
+++ b/src/Data/LazyNondet/Generic.lhs
@@ -12,7 +12,7 @@
 >
 > module Data.LazyNondet.Generic (
 >
->   Generic(..), GenericOps, generic, primitive, nondet, consLabels,
+>   Generic(..), GenericOps, generic, primitive, consLabels,
 >
 >   ApplyCons(..), Decons, (!), cons
 >
@@ -50,17 +50,6 @@
 > primitive :: Generic a => NormalForm -> a
 > primitive = fromJust . prim genericOps
 
-We also provide a generic operation `nondet` to translate instances of
-`Generic` into non-deterministic data.
-
-> nondet :: (Monad m, Generic a) => a -> Nondet cs m a
-> nondet = Typed . nf2hnf . generic
->
-> nf2hnf :: Monad m => NormalForm -> Untyped cs m
-> nf2hnf (Var _) = error "Primitive.nf2hnf: cannot convert logic variable"
-> nf2hnf (Fun _) = error "nf2hnf: conversion of function not yet implemented"
-> nf2hnf (Data label args) = return (Cons label (map nf2hnf args))
-
 The operation `consLabels` yields the list of constructors
 corresponding to a datatype `a`.
 
@@ -150,7 +139,9 @@
 Combinators
 -----------
 
-The combinator `(!)` used to enumerate the constructors of a datatype combines records with generic operations. The integer argument is used to label the different constructors.
+The combinator `(!)` used to enumerate the constructors of a datatype
+combines records with generic operations. The integer argument is used
+to label the different constructors.
 
 > infixr 0 !
 > (!) :: (Int -> GenericOps a) -> (Int -> GenericOps a) -> Int -> GenericOps a
diff --git a/src/Data/LazyNondet/HigherOrder.lhs b/src/Data/LazyNondet/HigherOrder.lhs
--- a/src/Data/LazyNondet/HigherOrder.lhs
+++ b/src/Data/LazyNondet/HigherOrder.lhs
@@ -49,9 +49,6 @@
 
 Here are private type classes that are used to implement `fun`.
 
-> newtype Lifted cs m a b
->   = Lifted { lifted :: Nondet cs m a -> Context cs -> ID -> Nondet cs m b }
-
 > class NestLambda a
 >  where
 >   type C a :: *
@@ -62,22 +59,24 @@
 
 Single-argument functions can be lifted using `lambda`.
 
-> instance NestLambda (Lifted cs m a b)
+> instance NestLambda (Nondet cs m a -> Context cs -> ID -> Nondet cs m b)
 >  where
->   type C (Lifted cs m a b) = cs
->   type M (Lifted cs m a b) = m
->   type T (Lifted cs m a b) = a -> b
+>   type C (Nondet cs m a -> Context cs -> ID -> Nondet cs m b) = cs
+>   type M (Nondet cs m a -> Context cs -> ID -> Nondet cs m b) = m
+>   type T (Nondet cs m a -> Context cs -> ID -> Nondet cs m b) = a -> b
 >
->   nestLambda = lambda . lifted
+>   nestLambda = lambda
 
 If we have a function on non-deterministic data we can lift it to the
 `Nondet` type with the following instance.
 
-> instance (NestLambda f, C f ~ cs, M f ~ m) => NestLambda (Nondet cs m a -> f)
+> instance (NestLambda (Nondet cs m b -> f),
+>           C (Nondet cs m b -> f) ~ cs, M  (Nondet cs m b -> f) ~ m)
+>       => NestLambda (Nondet cs m a -> Nondet cs m b -> f)
 >  where
->   type C (Nondet cs m a -> f) = cs
->   type M (Nondet cs m a -> f) = m
->   type T (Nondet cs m a -> f) = a -> T f
+>   type C (Nondet cs m a -> Nondet cs m b -> f) = cs
+>   type M (Nondet cs m a -> Nondet cs m b -> f) = m
+>   type T (Nondet cs m a -> Nondet cs m b -> f) = a -> T (Nondet cs m b -> f)
 >
 >   nestLambda f = lambda (\x _ _ -> nestLambda (f x))
 
@@ -98,33 +97,36 @@
 >
 > instance LiftFun (Nondet cs m a -> Nondet cs m b)
 >  where
->   type Lift (Nondet cs m a -> Nondet cs m b) = Lifted cs m a b
+>   type Lift (Nondet cs m a -> Nondet cs m b)
+>     = Nondet cs m a -> Context cs -> ID -> Nondet cs m b
 >
->   liftFun f = Lifted (\x _ _ -> f x)
+>   liftFun f x _ _ = f x
 >
 > instance LiftFun (Nondet cs m a -> Context cs -> Nondet cs m b)
 >  where
->   type Lift (Nondet cs m a -> Context cs -> Nondet cs m b) = Lifted cs m a b
+>   type Lift (Nondet cs m a -> Context cs -> Nondet cs m b)
+>     = Nondet cs m a -> Context cs -> ID -> Nondet cs m b
 >
->   liftFun f = Lifted (\x cs _ -> f x cs)
+>   liftFun f x cs _ = f x cs
 >
 > instance LiftFun (Nondet cs m a -> ID -> Nondet cs m b)
 >  where
->   type Lift (Nondet cs m a -> ID -> Nondet cs m b) = Lifted cs m a b
+>   type Lift (Nondet cs m a -> ID -> Nondet cs m b)
+>     = Nondet cs m a -> Context cs -> ID -> Nondet cs m b
 >
->   liftFun f = Lifted (\x _ u -> f x u)
+>   liftFun f x _ u = f x u
 >
 > instance LiftFun (Nondet cs m a -> Context cs -> ID -> Nondet cs m b)
 >  where
 >   type Lift (Nondet cs m a -> Context cs -> ID -> Nondet cs m b)
->           = Lifted cs m a b
+>     = Nondet cs m a -> Context cs -> ID -> Nondet cs m b
 >
->   liftFun = Lifted
+>   liftFun = id
 >
 > instance LiftFun (Nondet cs m b -> f)
 >       => LiftFun (Nondet cs m a -> Nondet cs m b -> f)
 >  where
 >   type Lift (Nondet cs m a -> Nondet cs m b -> f)
->           = Nondet cs m a -> Lift (Nondet cs m b -> f)
+>     = Nondet cs m a -> Lift (Nondet cs m b -> f)
 >
 >   liftFun f = liftFun . f
diff --git a/src/Data/LazyNondet/Matching.lhs b/src/Data/LazyNondet/Matching.lhs
--- a/src/Data/LazyNondet/Matching.lhs
+++ b/src/Data/LazyNondet/Matching.lhs
@@ -10,7 +10,7 @@
 >
 > module Data.LazyNondet.Matching (
 >
->   Match, match, ConsPatList(..), constructors, patterns,
+>   Match, ConsPatList(..), constructors, patterns,
 >
 >   withHNF, failure, caseOf, caseOf_
 >
@@ -137,6 +137,14 @@
 to be checked how big the slowdown of using `caseOf` is compared to
 using `withHNF` directly.
 
+
+Defining Constructor and Destructor Functions
+=============================================
+
+We provide combinators `constructors` and `destructors` that can be
+used to define functions for constructing and matching
+non-deterministic values.
+
 > class MkCons a
 >  where
 >   type Ctx a :: *
@@ -160,47 +168,47 @@
 >   type Res (Nondet cs m a -> b) = Res b
 >
 >   mkCons l xs x = mkCons l (untyped x:xs)
-
+>
 > infixr 0 :!
 >
 > data ConsPatList a b = a :! b
-
+>
 > class ConsList a
 >  where
 >   type CData a
 >
 >   consList :: [ConsLabel] -> a
-
+>
 > instance ConsList ()
 >  where
 >   type CData () = ()
 >   consList _ = ()
-
+>
 > instance (MkCons a, ConsList b) => ConsList (ConsPatList a b)
 >  where
 >   type CData (ConsPatList a b) = Res a
 >
 >   consList (l:ls) = mkCons l [] :! consList ls
 >   consList _ = error "consList: insufficient cons labels"
-
+>
 > constructors :: (ConsList a, Generic (CData a)) => a
 > constructors = cs
 >  where cs = consList (consLabels (undefined `asCDataOf` cs))
 >
 > asCDataOf :: ConsList a => CData a -> a -> CData a
 > asCDataOf = const
-
+>
 > class PatternList a
 >  where
 >   type PData a
 >
 >   patternList :: [ConsLabel] -> a
-
+>
 > instance PatternList ()
 >  where
 >   type PData () = ()
 >   patternList _ = ()
-
+>
 > instance (WithUntyped a, PatternList p, cs ~ C a, m ~ M a, b ~ T a)
 >       => PatternList (ConsPatList ((Context cs -> a) -> Match t cs m b) p)
 >  where
@@ -208,7 +216,7 @@
 >
 >   patternList (l:ls) = match (index l) :! patternList ls
 >   patternList _ = error "patternList: insufficient cons labels"
-
+>
 > patterns :: (PatternList a, Generic (PData a)) => a
 > patterns = cs
 >  where cs = patternList (consLabels (undefined `asPDataOf` cs))
diff --git a/src/Data/LazyNondet/Primitive.lhs b/src/Data/LazyNondet/Primitive.lhs
--- a/src/Data/LazyNondet/Primitive.lhs
+++ b/src/Data/LazyNondet/Primitive.lhs
@@ -1,19 +1,16 @@
 % Primitive Generic Functions on Lazy Non-Deterministic Data
 % Sebastian Fischer (sebf@informatik.uni-kiel.de)
 
-> {-# LANGUAGE
->       FlexibleContexts
->   #-}
->
 > module Data.LazyNondet.Primitive (
 >
->   groundNormalForm, partialNormalForm,
+>   nondet, groundNormalForm, partialNormalForm,
 >
 >   prim_eq
 >
 > ) where
 >
 > import Data.LazyNondet.Types
+> import Data.LazyNondet.Generic
 >
 > import Control.Monad.State
 > import Control.Monad.Update
@@ -21,8 +18,26 @@
 > import Control.Constraint.Choice
 >
 > import Data.Supply
+
+We provide a generic operation `nondet` to translate instances of
+`Generic` into non-deterministic data.
+
+> nondet :: (Update cs m m, Generic a) => a -> Nondet cs m a
+> nondet = Typed . return . nf2hnf . generic
 >
+> nf2hnf :: Update cs m m => NormalForm -> HeadNormalForm cs m
+> nf2hnf (Var _) = error "Primitive.nf2hnf: cannot convert logic variable"
+> nf2hnf (Data label args) = Cons label (map (return . nf2hnf) args)
+> nf2hnf (Fun f) = Lambda (\x _ _ -> liftM (nf2hnf . f) $ gnf x)
+>  where gnf x = groundNormalForm (Typed x) $
+>                  error "Primitive.nf2hnf: primitive function uses context"
 
+The `...NormalForm` functions evaluate a non-deterministic value and
+lift all non-deterministic choices to the top level. The results are
+deterministic values and can be converted into their Haskell
+representation. Partial normal forms may contain unbound logic
+variables while ground normal forms are data terms.
+
 > groundNormalForm :: Update cs m m'
 >                  => Nondet cs m a -> Context cs -> m' NormalForm
 > groundNormalForm x (Context cs) = evalStateT (gnf (untyped x)) cs
@@ -31,11 +46,13 @@
 >                   => Nondet cs m a -> Context cs -> m' NormalForm
 > partialNormalForm x (Context cs) = evalStateT (pnf (untyped x)) cs
 
-The `...NormalForm` functions evaluate a non-deterministic value and
-lift all non-deterministic choices to the top level. The results are
-deterministic values and can be converted into their Haskell
-representation. Partial normal forms may contain unbound logic
-variables while ground normal forms are data terms.
+To compute ground normal forms, we ignore free variables and narrow
+them to ground terms. To compute partial normal forms, we do not
+narrow unbound variables and in a second phase bind those variables
+that were bound after we have visited them. For example, when
+computing the normal form of `let x free in (x,not x)` we don't know
+that `x` will be bound in the result when we encounter it for the
+first time.
 
 > gnf :: Update cs m m' => Untyped cs m -> StateT cs m' NormalForm
 > gnf = nf (\_ _ -> Just ()) Data mkVar Fun
@@ -49,13 +66,8 @@
 >    = nf lookupChoice ((return.).Cons) ((return.).FreeVar) (return.Lambda) x
 >  >>= nf lookupChoice Data mkVar Fun
 
-To compute ground normal forms, we ignore free variables and narrow
-them to ground terms. To compute partial normal forms, we do not
-narrow unbound variables and in a second phase bind those variables
-that were bound after we have visited them. For example, when
-computing the normal form of `let x free in (x,not x)` we don't know
-that `x` will be bound in the result when we encounter it for the
-first time.
+The `nf` function is used by all normal-form functions and performs
+all the work.
 
 > nf :: Update cs m m'
 >    => (Int -> cs -> Maybe a)
@@ -75,8 +87,9 @@
 >       return (cns label nfs)
 >     Lambda _ -> return . fun $ error "Data.LazyNondet.Primitive.nf: function"
 
-The `nf` function is used by all normal-form functions and performs
-all the work.
+We provide a generic comparison function for untyped non-deterministic
+data that is used to define a typed equality test in the
+`Data.LazyNondet.Types.Bool` module.
 
 > prim_eq :: Update cs m m
 >         => Untyped cs m -> Untyped cs m -> StateT cs m Bool
@@ -91,9 +104,9 @@
 >     if eq then all_eq vs ws else return False
 >   all_eq _ _ = return False
 
-We provide a generic comparison function for untyped non-deterministic
-data that is used to define a typed equality test in the
-`Data.LazyNondet.Types.Bool` module.
+The function `solveCons` is like `solve` but always yields a
+constructor-rooted term, i.e., no free variable or delayed
+computation.
 
 > solveCons :: Update cs m m
 >           => Untyped cs m -> StateT cs m (HeadNormalForm cs m)
@@ -104,8 +117,4 @@
 >     Delayed _ res -> get >>= solveCons . res . Context
 >     Lambda _ -> error "Data.LazyNondet.Primitive.solveCons: matched lambda"
 >     _ -> return hnf
-
-The function `solveCons` is like `solve` but always yields a
-constructor-rooted term, i.e., no free variable or delayed
-computation.