diff --git a/Test.lhs b/Test.lhs
--- a/Test.lhs
+++ b/Test.lhs
@@ -7,9 +7,10 @@
 
 > import Test.HUnit
 > import Control.CFLP.Tests.CallTimeChoice as CTC
+> import Control.CFLP.Tests.HigherOrder as HO
 >
 > main :: IO ()
 > main = do
->  runTestTT $ test [CTC.tests]
+>  runTestTT $ test [CTC.tests,HO.tests]
 >  return ()
 
diff --git a/cflp.cabal b/cflp.cabal
--- a/cflp.cabal
+++ b/cflp.cabal
@@ -1,5 +1,5 @@
 Name:          cflp
-Version:       2009.1.6
+Version:       2009.1.13
 Cabal-Version: >= 1.6
 Synopsis:      Constraint Functional-Logic Programming in Haskell
 Description:   This package provides combinators for constraint
@@ -38,8 +38,10 @@
                     Data.LazyNondet.Matching,
                     Data.LazyNondet.Narrowing,
                     Data.LazyNondet.Primitive,
+                    Data.LazyNondet.HigherOrder,
                     Control.CFLP.Tests,
                     Control.CFLP.Tests.CallTimeChoice
+                    Control.CFLP.Tests.HigherOrder
   Hs-Source-Dirs:   src
   Extensions:       FunctionalDependencies,
                     MultiParamTypeClasses,
diff --git a/src/Control/CFLP.lhs b/src/Control/CFLP.lhs
--- a/src/Control/CFLP.lhs
+++ b/src/Control/CFLP.lhs
@@ -17,15 +17,11 @@
 >
 >   Strategy, depthFirst,
 >
->   module Data.LazyNondet,
->   module Data.LazyNondet.Types.Bool,
->   module Data.LazyNondet.Types.List
+>   module Data.LazyNondet
 >
 > ) where
 >
 > import Data.LazyNondet
-> import Data.LazyNondet.Types.Bool
-> import Data.LazyNondet.Types.List
 >
 > import Control.Monad.State
 > import Control.Monad.Update
@@ -46,10 +42,10 @@
 
 > type CS = ChoiceStoreIM
 >
-> noConstraints :: CS
-> noConstraints = noChoices
+> noConstraints :: Context CS
+> noConstraints = Context noChoices
 >
-> type Computation m a = CS -> ID -> Nondet CS (UpdateT CS m) a
+> type Computation m a = Context CS -> ID -> Nondet CS (UpdateT CS m) a
 
 Currently, the constraint store used to evaluate constraint
 functional-logic programs is simply a `ChoiceStore`. It will be a
@@ -67,8 +63,8 @@
 The strategy of the list monad is depth-first search.
 
 > evaluate :: (CFLP CS m, Update CS m m')
->          => (Nondet CS m a -> CS -> m' b)
->          -> Strategy m' -> (CS -> ID -> Nondet CS m a)
+>          => (Nondet CS m a -> Context CS -> m' b)
+>          -> Strategy m' -> (Context CS -> ID -> Nondet CS m a)
 >          -> IO [b]
 > evaluate evalNondet enumerate op = do
 >   i <- initID
@@ -78,13 +74,13 @@
 constraint functional-logic computation according to a given strategy.
 
 > eval, evalPartial :: (CFLP CS m, Update CS m m', Data a)
->                   => Strategy m' -> (CS -> ID -> Nondet CS m a)
+>                   => Strategy m' -> (Context CS -> ID -> Nondet CS m a)
 >                   -> IO [a]
 > eval        s = liftM (map prim) . evaluate groundNormalForm  s
 > evalPartial s = liftM (map prim) . evaluate partialNormalForm s
 >
 > evalPrint :: (CFLP CS m, Update CS m m', Data a, Show a)
->           => Strategy m' -> (CS -> ID -> Nondet CS m a)
+>           => Strategy m' -> (Context CS -> ID -> Nondet CS m a)
 >           -> IO ()
 > evalPrint s op = evaluate partialNormalForm s op >>= printSols
 >
@@ -102,8 +98,8 @@
 
 We provide
 
-  * an `eval` operation to compute Haskell terms from non-determinitic
-    data,
+  * an `eval` operation to compute Haskell terms from
+    non-deterministic data,
 
   * an operation `evalPartial` to compute partial Haskell terms where
     logic variables are replaced with an error, and
diff --git a/src/Control/CFLP/Tests/CallTimeChoice.lhs b/src/Control/CFLP/Tests/CallTimeChoice.lhs
--- a/src/Control/CFLP/Tests/CallTimeChoice.lhs
+++ b/src/Control/CFLP/Tests/CallTimeChoice.lhs
@@ -12,17 +12,17 @@
 > import Control.CFLP.Tests
 > import Test.HUnit
 >
-> import Control.CFLP
->
 > import Prelude hiding ( not, null, head )
+> import Data.LazyNondet.Types.Bool
+> import Data.LazyNondet.Types.List
 >
 > tests :: Test
 > tests = "call-time choice" ~: test
->  [ "ignore first, narrow second" ~: ignoreFirstNarrowSecond
->  , "shared vars are equal" ~: sharedVarsAreEqual
->  , "no demand on shared var" ~: noDemandOnSharedVar
->  , "shared compound terms" ~: sharedCompoundTerms
->  ]
+>   [ "ignore first, narrow second" ~: ignoreFirstNarrowSecond
+>   , "shared vars are equal" ~: sharedVarsAreEqual
+>   , "no demand on shared var" ~: noDemandOnSharedVar
+>   , "shared compound terms" ~: sharedCompoundTerms
+>   ]
 
 Every module under `Control.CFLP.Tests` defines a constant `tests`
 that collects all defined tests.
@@ -33,7 +33,7 @@
 >   comp cs u = ignot (error "illegal demand") (unknown u) cs
 >
 > ignot :: CFLP cs m
->       => Nondet cs m a -> Nondet cs m Bool -> cs -> Nondet cs m Bool
+>       => Nondet cs m a -> Nondet cs m Bool -> Context cs -> Nondet cs m Bool
 > ignot _ = not
 
 This test checks a function with two arguments, where the first must
@@ -73,7 +73,8 @@
 >  where
 >   comp cs u = negHeads (unknown u) cs
 >
-> negHeads :: CFLP cs m => Nondet cs m [Bool] -> cs -> Nondet cs m [Bool]
+> negHeads :: CFLP cs m
+>          => Nondet cs m [Bool] -> Context cs -> Nondet cs m [Bool]
 > negHeads l cs = not (head l cs) cs ^: head l cs ^: nil
 
 This test checks whether sharing is ensured on aruments of compound
diff --git a/src/Control/CFLP/Tests/HigherOrder.lhs b/src/Control/CFLP/Tests/HigherOrder.lhs
new file mode 100644
--- /dev/null
+++ b/src/Control/CFLP/Tests/HigherOrder.lhs
@@ -0,0 +1,78 @@
+% Testing Higher-Order Functional-Logic Operations
+% Sebastian Fischer (sebf@informatik.uni-kiel.de)
+
+This module defines tests that show how to define higher-order
+functional-logic programs.
+
+> module Control.CFLP.Tests.HigherOrder where
+>
+> import Control.CFLP
+> import Control.CFLP.Tests
+> import Test.HUnit
+>
+> import Prelude hiding ( not, null, head, map, foldr )
+> import Data.LazyNondet.Types.Bool
+> import Data.LazyNondet.Types.List
+>
+> tests :: Test
+> tests = "higher order" ~: test
+>   [ "apply not function" ~: applyNotFunction
+>   , "apply binary constructor" ~: applyBinCons
+>   , "apply non-deterministic choice" ~: applyChoice
+>   , "call-time choice" ~: callTimeChoice
+>   , "map shared unknowns" ~: mapSharedUnknowns
+>   , "memeber with fold" ~: memberWithFold
+>   ]
+
+The following test simply applies the not function.
+
+> applyNotFunction :: Assertion
+> applyNotFunction = assertResults comp [True]
+>  where
+>   comp = apply (fun not) false
+
+The following test applies the binary list constructor.
+
+> applyBinCons :: Assertion
+> applyBinCons = assertResults comp [[True]]
+>  where
+>   comp cs = withUnique $ \u1 u2 ->
+>               apply (apply (fun (^:)) true cs u1) nil cs u2
+
+The following tests applies the binary operator for non-deterministic
+choice.
+
+> applyChoice :: Assertion
+> applyChoice = assertResults comp [False,True]
+>  where
+>   comp cs = withUnique $ \u1 u2 ->
+>               apply (apply (fun (?)) false cs u1) true cs u2
+
+The following test checks whether call-time choice is still obtained
+when applying the choice combinator using higher-order features.
+
+> callTimeChoice :: Assertion
+> callTimeChoice = assertResults comp [[False,False],[True,True]]
+>  where
+>   comp cs = withUnique $ \u1 u2 u3 ->
+>               apply (fun two)
+>                     (apply (apply (fun (?)) false cs u1) true cs u2) cs u3
+>
+> two :: Monad m => Nondet cs m a -> Nondet cs m [a]
+> two x = x ^: x ^: nil
+
+The following test maps the function `not` over a list with a
+duplicated free variable.
+
+> mapSharedUnknowns :: Assertion
+> mapSharedUnknowns = assertResults comp [[True,True],[False,False]]
+>  where
+>   comp cs = withUnique $ \u -> map (fun not) (two (unknown u)) cs
+
+The following test checks the member operation defined using `foldr`.
+
+> memberWithFold :: Assertion
+> memberWithFold = assertResults comp [True,False]
+>  where
+>   comp = foldr (fun (?)) failure (true ^: false ^: nil)
+
diff --git a/src/Control/Constraint/Choice.lhs b/src/Control/Constraint/Choice.lhs
--- a/src/Control/Constraint/Choice.lhs
+++ b/src/Control/Constraint/Choice.lhs
@@ -46,7 +46,7 @@
 >  where
 >   lookupChoice u (ChoiceStoreIM cs) = IM.lookup u cs
 >
->   assertChoice _ u x (ChoiceStoreIM cs) = do
+>   assertChoice _ u x (ChoiceStoreIM cs) =
 >     maybe (return (ChoiceStoreIM (IM.insert u x cs)))
 >           (\y -> do guard (x==y); return (ChoiceStoreIM cs))
 >           (IM.lookup u cs)
diff --git a/src/Control/Monad/Update.lhs b/src/Control/Monad/Update.lhs
--- a/src/Control/Monad/Update.lhs
+++ b/src/Control/Monad/Update.lhs
@@ -110,7 +110,7 @@
 >     run x = lift (lift (unUpdateT x)) >>= doUpdate
 >
 >     doUpdate (Return a)     = return a
->     doUpdate (Update upd y) = do lift (update upd); update upd; run y
+>     doUpdate (Update upd y) = do update upd; lift (update upd); run y
 
 We define another instance of `Update` where results are not returned
 in the base monad but in the transformed base monad. This instance is
diff --git a/src/Data/LazyNondet.lhs b/src/Data/LazyNondet.lhs
--- a/src/Data/LazyNondet.lhs
+++ b/src/Data/LazyNondet.lhs
@@ -6,7 +6,7 @@
 
 > module Data.LazyNondet (
 >
->   NormalForm, Nondet,
+>   NormalForm, Nondet, Context(..),
 >
 >   ID, initID, withUnique,
 >
@@ -20,6 +20,8 @@
 >
 >   ConsRep(..), cons, match,
 >
+>   apply, fun
+>
 > ) where
 >
 > import Data.Data
@@ -28,3 +30,4 @@
 > import Data.LazyNondet.Matching
 > import Data.LazyNondet.Narrowing
 > import Data.LazyNondet.Primitive
+> import Data.LazyNondet.HigherOrder
diff --git a/src/Data/LazyNondet/HigherOrder.lhs b/src/Data/LazyNondet/HigherOrder.lhs
new file mode 100644
--- /dev/null
+++ b/src/Data/LazyNondet/HigherOrder.lhs
@@ -0,0 +1,109 @@
+% Higher-Order Non-Deterministic Operations
+% Sebastian Fischer (sebf@informatik.uni-kiel.de)
+
+This module defines combinators for higher-order CFLP.
+
+> {-# LANGUAGE 
+>       MultiParamTypeClasses, NoMonomorphismRestriction,
+>       FunctionalDependencies,
+>       TypeSynonymInstances,
+>       UndecidableInstances,
+>       FlexibleInstances,
+>       FlexibleContexts
+>   #-}
+>
+> module Data.LazyNondet.HigherOrder (
+>
+>   fun, apply
+>
+> ) where
+>
+> import Data.LazyNondet.Types
+> import Data.LazyNondet.Matching ( withHNF )
+>
+> import Control.Monad.Update
+
+With the `lambda` combinator functions on non-deterministic data are
+lifted to the `Nondet` type.
+
+> lambda :: Monad m
+>        => (Nondet cs m a -> Context cs -> ID -> Nondet cs m b)
+>        -> Nondet cs m (a -> b)
+> lambda f = Typed . return $ Lambda (\x cs -> untyped . f (Typed x) cs)
+
+To apply a lambda, we provide the combinator `apply`.
+
+> apply :: Update cs m m
+>       => Nondet cs m (a -> b) -> Nondet cs m a
+>       -> Context cs -> ID -> Nondet cs m b
+> apply f x cs u = withHNF f (\f cs ->
+>   case f of
+>     Lambda f -> Typed (f (untyped x) cs u)
+>     FreeVar _ f -> apply (Typed f) x cs u
+>     _ -> error "Data.LazyNondet.HigherOrder: cannot apply") cs
+
+The overloaded operation `fun` converts a function on
+non-deterministic data (of arbitrary arity) into a (possibly nested)
+lambda.
+
+> fun :: (Monad m, LiftFun f g, NestLambda g cs m t)
+>     => f -> Nondet cs m t
+> fun = nestLambda . liftFun
+
+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 cs m b | a -> cs, a -> m, a -> b
+>  where
+>   nestLambda :: Monad m => a -> Nondet cs m b
+
+Single-argument functions can be lifted using `lambda`.
+
+> instance NestLambda (Lifted cs m a b) cs m (a -> b)
+>  where
+>   nestLambda = lambda . lifted
+
+If we have a function on non-deterministic data we can lift it to the
+`Nondet` type with the following instance.
+
+> instance NestLambda f cs m b => NestLambda (Nondet cs m a -> f) cs m (a -> b)
+>  where
+>   nestLambda f = lambda (\x _ _ -> nestLambda (f x))
+
+We provide a combinator `liftFun` for 
+
+  * constructor functions that do not take a constraint store or a
+    unique id,
+
+  * deterministic functions that only take a constraint store, and
+
+  * non-deterministic functions that only take a unique id.
+
+> class LiftFun f g | f -> g
+>  where
+>   liftFun :: f -> g
+>
+> instance LiftFun (Nondet cs m a -> Nondet cs m b) (Lifted cs m a b)
+>  where
+>   liftFun f = Lifted (\x _ _ -> f x)
+>
+> instance LiftFun (Nondet cs m a -> Context cs -> Nondet cs m b)
+>                  (Lifted cs m a b)
+>  where
+>   liftFun f = Lifted (\x cs _ -> f x cs)
+>
+> instance LiftFun (Nondet cs m a -> ID -> Nondet cs m b) (Lifted cs m a b)
+>  where
+>   liftFun f = Lifted (\x _ u -> f x u)
+>
+> instance LiftFun (Nondet cs m a -> Context cs -> ID -> Nondet cs m b)
+>                  (Lifted cs m a b)
+>  where
+>   liftFun = Lifted
+>
+> instance LiftFun (Nondet cs m b -> f) g => 
+>          LiftFun (Nondet cs m a -> Nondet cs m b -> f) (Nondet cs m a -> g)
+>  where
+>   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
@@ -24,13 +24,13 @@
 > import Control.Monad.State
 > import Control.Monad.Update
 >
-> withHNF :: (Monad m, Update cs m m)
+> withHNF :: Update cs m m
 >         => Nondet cs m a
->         -> (HeadNormalForm cs m -> cs -> Nondet cs m b)
->         -> cs -> Nondet cs m b
-> withHNF x b cs = Typed (do
+>         -> (HeadNormalForm cs m -> Context cs -> Nondet cs m b)
+>         -> Context cs -> Nondet cs m b
+> withHNF x b (Context cs) = Typed (do
 >   (hnf,cs') <- runStateT (updateState (untyped x)) cs
->   untyped (b hnf cs'))
+>   untyped (b hnf (Context cs')))
 
 The `withHNF` operation can be used for pattern matching and solves
 constraints associated to the head constructor of a non-deterministic
@@ -96,11 +96,13 @@
 the list of untyped values and yields the result of applying the given
 function to typed versions of these values.
 
-> newtype Match a cs m b = Match { unMatch :: (ConIndex, cs -> Branch cs m b) }
+> newtype Match a cs m b
+>   = Match { unMatch :: (ConIndex, Context cs -> Branch cs m b) }
+>
 > type Branch cs m a = [Untyped cs m] -> Nondet cs m a
 >
 > match :: (ConsRep a, WithUntyped b)
->       => a -> (C b -> b) -> Match t (C b) (M b) (T b)
+>       => a -> (Context (C b) -> b) -> Match t (C b) (M b) (T b)
 > match c alt = Match (constrIndex (consRep c), withUntyped . alt)
 
 The operation `match` is used to build destructor functions for
@@ -112,12 +114,12 @@
 Failure is just a type version of `mzero`.
 
 > caseOf :: Update cs m m
->        => Nondet cs m a -> [Match a cs m b] -> cs -> Nondet cs m b
+>        => Nondet cs m a -> [Match a cs m b] -> Context cs -> Nondet cs m b
 > caseOf x bs = caseOf_ x bs failure
 >
 > caseOf_ :: Update cs m m
 >         => Nondet cs m a -> [Match a cs m b] -> Nondet cs m b
->         -> cs -> Nondet cs m b
+>         -> Context cs -> Nondet cs m b
 > caseOf_ x bs def =
 >   withHNF x $ \hnf cs ->
 >   case hnf of
@@ -127,6 +129,7 @@
 >       | otherwise -> caseOf_ (Typed (res cs)) bs def cs
 >     Cons _ idx args ->
 >       maybe def (\b -> b cs args) (lookup idx (map unMatch bs))
+>     Lambda _ -> error "Data.LazyNondet.Matching.caseOf: cannot match lambda"
 
 We provide operations `caseOf_` and `caseOf` (with and without a
 default alternative) for more convenient pattern matching. The untyped
diff --git a/src/Data/LazyNondet/Narrowing.lhs b/src/Data/LazyNondet/Narrowing.lhs
--- a/src/Data/LazyNondet/Narrowing.lhs
+++ b/src/Data/LazyNondet/Narrowing.lhs
@@ -24,15 +24,15 @@
 > unknown :: (MonadUpdate cs m, Narrow cs a) => ID -> Nondet cs m a
 > unknown u = freeVar u (delayed (redelay u) (\cs -> narrow cs u))
 >
-> redelay :: ChoiceStore cs => ID -> cs -> Bool
-> redelay (ID us) = isNothing . lookupChoice (supplyValue us)
+> redelay :: ChoiceStore cs => ID -> Context cs -> Bool
+> redelay (ID us) (Context cs) = isNothing . lookupChoice (supplyValue us) $ cs
 
 The application of `unknown` to a constraint store and a unique
 identifier represents a logic variable of an arbitrary type. 
 
 > class ChoiceStore cs => Narrow cs a
 >  where
->   narrow :: MonadUpdate cs m => cs -> ID -> Nondet cs m a
+>   narrow :: MonadUpdate cs m => Context cs -> ID -> Nondet cs m a
 
 Logic variables of type `a` can be narrowed to head-normal form if
 there is an instance of the type class `Narrow`. A constraint store
@@ -52,8 +52,9 @@
 executions and *not* reexecuted.
 
 > oneOf :: (MonadUpdate cs m, ChoiceStore cs)
->       => [Nondet cs m a] -> cs -> ID -> Nondet cs m a
-> oneOf xs cs (ID us) = Typed (choice cs (supplyValue us) (map untyped xs))
+>       => [Nondet cs m a] -> Context cs -> ID -> Nondet cs m a
+> oneOf xs (Context cs) (ID us)
+>   = Typed (choice cs (supplyValue us) (map untyped xs))
 
 The operation `oneOf` takes a list of non-deterministic values and
 returns a non-deterministic value that yields one of the elements in
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
@@ -40,7 +40,7 @@
 > generic x = NormalForm (toConstr x) (gmapQ generic x)
 >
 > nf2hnf :: Monad m => NormalForm -> Untyped cs m
-> nf2hnf (Var _) = error $ "Primitive.nf2hnf: cannot convert logic variable"
+> nf2hnf (Var _) = error "Primitive.nf2hnf: cannot convert logic variable"
 > nf2hnf (NormalForm con args) = return (mkHNF con (map nf2hnf args))
 >
 > nondet :: (Monad m, Data a) => a -> Nondet cs m a
@@ -49,12 +49,13 @@
 We also provide a generic operation `nondet` to translate instances of
 the `Data` class into non-deterministic data.
 
-> groundNormalForm :: Update cs m m' => Nondet cs m a -> cs -> m' NormalForm
-> groundNormalForm = evalStateT . gnf . untyped
+> groundNormalForm :: Update cs m m'
+>                  => Nondet cs m a -> Context cs -> m' NormalForm
+> groundNormalForm x (Context cs) = evalStateT (gnf (untyped x)) cs
 >
 > partialNormalForm :: (Update cs m m', ChoiceStore cs)
->                   => Nondet cs m a -> cs -> m' NormalForm
-> partialNormalForm = evalStateT . pnf . untyped
+>                   => 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
@@ -92,10 +93,11 @@
 >     FreeVar u@(ID us) y ->
 >       get >>= maybe (return (fv u y)) (const (nf lkp cns fv y))
 >             . lkp (supplyValue us)
->     Delayed _ resume -> get >>= nf lkp cns fv . resume
+>     Delayed _ resume -> get >>= nf lkp cns fv . resume . Context
 >     Cons typ idx args -> do
 >       nfs <- mapM (nf lkp cns fv) args
 >       return (cns (indexConstr typ idx) nfs)
+>     Lambda _ -> error "Data.LazyNondet.Primitive.nf: cannot convert lambda"
 
 The `nf` function is used by all normal-form functions and performs
 all the work.
@@ -123,7 +125,7 @@
 >   hnf <- updateState x
 >   case hnf of
 >     FreeVar _ y -> solveCons y
->     Delayed _ res -> get >>= solveCons . res
+>     Delayed _ res -> get >>= solveCons . res . Context
 >     _ -> return hnf
 
 The function `solveCons` is like `solve` but always yields a
diff --git a/src/Data/LazyNondet/Types.lhs b/src/Data/LazyNondet/Types.lhs
--- a/src/Data/LazyNondet/Types.lhs
+++ b/src/Data/LazyNondet/Types.lhs
@@ -11,8 +11,10 @@
 >
 > module Data.LazyNondet.Types (
 >
->   ID(..), NormalForm(..), HeadNormalForm(..), Untyped, Nondet(..),
+>   Context(..), ID(..), 
 >
+>   NormalForm(..), HeadNormalForm(..), Untyped, Nondet(..),
+>
 >   mkHNF, freeVar, delayed
 >
 > ) where
@@ -23,6 +25,8 @@
 >
 > import Data.Supply
 >
+> newtype Context cs = Context cs
+>
 > newtype ID = ID (Supply Int)
 >
 > data NormalForm = NormalForm Constr [NormalForm] | Var Int
@@ -36,7 +40,8 @@
 > data HeadNormalForm cs m
 >   = Cons DataType ConIndex [Untyped cs m]
 >   | FreeVar ID (Untyped cs m)
->   | Delayed (cs -> Bool) (cs -> Untyped cs m)
+>   | Delayed (Context cs -> Bool) (Context cs -> Untyped cs m)
+>   | Lambda (Untyped cs m -> Context cs -> ID -> Untyped cs m)
 >
 > type Untyped cs m = m (HeadNormalForm cs m)
 
@@ -69,7 +74,8 @@
 The function `freeVar` is used to put a name around a narrowed free
 variable.
 
-> delayed :: Monad m => (cs -> Bool) -> (cs -> Nondet cs m a) -> Nondet cs m a
+> delayed :: Monad m => (Context cs -> Bool) -> (Context cs -> Nondet cs m a)
+>         -> Nondet cs m a
 > delayed p resume = Typed . return . Delayed p $ (untyped . resume)
 
 With `delayed` computations can be delayed to be reexecuted with the
@@ -88,6 +94,7 @@
 >  where
 >   show (FreeVar (ID u) _) = '_':show (supplyValue u)
 >   show (Delayed _ _) = "<delayed>"
+>   show (Lambda _) = "<function>"
 >   show (Cons typ idx args) 
 >     | null args = show con
 >     | otherwise = unwords (('(':show con):map show args++[")"])
@@ -104,7 +111,8 @@
 > instance Show (HeadNormalForm cs (UpdateT cs []))
 >  where
 >   show (FreeVar (ID u) _)  = '_':show (supplyValue u)
->   show (Delayed _ _)         = "<delayed>"
+>   show (Delayed _ _)       = "<delayed>"
+>   show (Lambda _)          = "<function>"
 >   show (Cons typ idx [])   = show (indexConstr typ idx)
 >   show (Cons typ idx args) =
 >     "("++show (indexConstr typ idx)++" "++unwords (map show args)++")" 
diff --git a/src/Data/LazyNondet/Types/Bool.lhs b/src/Data/LazyNondet/Types/Bool.lhs
--- a/src/Data/LazyNondet/Types/Bool.lhs
+++ b/src/Data/LazyNondet/Types/Bool.lhs
@@ -26,13 +26,13 @@
 > true :: Monad m => Nondet cs m Bool
 > true = cons True
 >
-> pTrue :: (cs -> Nondet cs m a) -> Match Bool cs m a
+> pTrue :: (Context cs -> Nondet cs m a) -> Match Bool cs m a
 > pTrue = match True
 >
 > false :: Monad m => Nondet cs m Bool
 > false = cons False
 >
-> pFalse :: (cs -> Nondet cs m a) -> Match Bool cs m a
+> pFalse :: (Context cs -> Nondet cs m a) -> Match Bool cs m a
 > pFalse = match False
 
 In order to be able to use logic variables of boolean type, we make it
@@ -44,11 +44,11 @@
 
 Some operations with `Bool`s:
 
-> not :: Update cs m m => Nondet cs m Bool -> cs -> Nondet cs m Bool
+> not :: Update cs m m => Nondet cs m Bool -> Context cs -> Nondet cs m Bool
 > not x = caseOf_ x [pFalse (const true)] false
 >
 > (===) :: Update cs m m
->       => Nondet cs m a -> Nondet cs m a -> cs -> Nondet cs m Bool
-> (x === y) cs = Typed $ do
+>       => Nondet cs m a -> Nondet cs m a -> Context cs -> Nondet cs m Bool
+> (x === y) (Context cs) = Typed $ do
 >   eq <- evalStateT (prim_eq (untyped x) (untyped y)) cs
 >   untyped $ if eq then true else false
diff --git a/src/Data/LazyNondet/Types/List.lhs b/src/Data/LazyNondet/Types/List.lhs
--- a/src/Data/LazyNondet/Types/List.lhs
+++ b/src/Data/LazyNondet/Types/List.lhs
@@ -19,24 +19,27 @@
 >
 > import Control.Constraint.Choice
 >
+> import Prelude hiding ( map, foldr )
+> import qualified Prelude as P
+>
 > instance ConsRep [()] where consRep = toConstr
 >
 > nil :: Monad m => Nondet cs m [a]
 > nil = cons ([] :: [()])
 >
-> pNil :: (cs -> Nondet cs m b) -> Match [a] cs m b
+> pNil :: (Context cs -> Nondet cs m b) -> Match [a] cs m b
 > pNil = match ([] :: [()])
 >
 > infixr 5 ^:
 > (^:) :: Monad m => Nondet cs m a -> Nondet cs m [a] -> Nondet cs m [a]
 > (^:) = cons ((:) :: () -> [()] -> [()])
 >
-> pCons :: (cs -> Nondet cs m a -> Nondet cs m [a] -> Nondet cs m b)
+> pCons :: (Context cs -> Nondet cs m a -> Nondet cs m [a] -> Nondet cs m b)
 >       -> Match [a] cs m b
 > pCons = match ((:) :: () -> [()] -> [()])
 >
 > fromList :: Monad m => [Nondet cs m a] -> Nondet cs m [a]
-> fromList = foldr (^:) nil
+> fromList = P.foldr (^:) nil
 
 We can use logic variables of a list type if there are logic variables
 for the element type.
@@ -48,12 +51,29 @@
 
 Some operations on lists:
 
-> null :: Update cs m m => Nondet cs m [a] -> cs -> Nondet cs m Bool
+> null :: Update cs m m => Nondet cs m [a] -> Context cs -> Nondet cs m Bool
 > null xs = caseOf_ xs [pNil (const true)] false
 >
-> head :: Update cs m m => Nondet cs m [a] -> cs -> Nondet cs m a
+> head :: Update cs m m => Nondet cs m [a] -> Context cs -> Nondet cs m a
 > head l = caseOf l [pCons (\_ x _ -> x)]
 >
-> tail :: Update cs m m => Nondet cs m [a] -> cs -> Nondet cs m [a]
+> tail :: Update cs m m => Nondet cs m [a] -> Context cs -> Nondet cs m [a]
 > tail l = caseOf l [pCons (\_ _ xs -> xs)]
+
+Higher-order functions:
+
+> map :: Update cs m m
+>     => Nondet cs m (a -> b) -> Nondet cs m [a]
+>     -> Context cs -> ID -> Nondet cs m [b]
+> map f l cs = withUnique $ \u ->
+>               foldr (fun (\x xs -> apply f x cs u ^: xs)) nil l cs
+>
+> foldr :: Update cs m m
+>       => Nondet cs m (a -> b -> b) -> Nondet cs m b -> Nondet cs m [a]
+>       -> Context cs -> ID -> Nondet cs m b
+> foldr f y l cs = withUnique $ \u1 u2 u3 ->
+>   caseOf l
+>     [ pNil (const y)
+>     , pCons (\cs x xs -> apply (apply f x cs u1) (foldr f y xs cs u2) cs u3)
+>     ] cs