diff --git a/Curry/AbstractCurry.hs b/Curry/AbstractCurry.hs
--- a/Curry/AbstractCurry.hs
+++ b/Curry/AbstractCurry.hs
@@ -28,6 +28,7 @@
 		      CField,
                       readCurry, writeCurry) where
 
+import Control.Monad(liftM)
 import Data.List(intersperse)
 
 import Curry.Files.PathUtils (writeModule,readModule)
@@ -258,10 +259,7 @@
 -- Reads an AbstractCurry file and returns the corresponding AbstractCurry
 -- program term (type 'CurryProg')
 readCurry :: String -> IO CurryProg
-readCurry filename
-   = do file <- readModule filename
-	let prog = (read file) :: CurryProg
-	return prog
+readCurry = liftM read . readModule
 
 -- Writes an AbstractCurry program term into a file
 -- If the flag is set, it will be the hidden .curry sub directory.
@@ -275,8 +273,8 @@
 showCurry (CurryProg mname imps types funcs ops) =
   "CurryProg "++show mname++"\n "++
   show imps ++"\n ["++
-  concat (intersperse ",\n  " (map (\t->show t) types)) ++"]\n ["++
-  concat (intersperse ",\n  " (map (\f->show f) funcs)) ++"]\n "++
+  concat (intersperse ",\n  " (map show types)) ++"]\n ["++
+  concat (intersperse ",\n  " (map show funcs)) ++"]\n "++
   show ops ++"\n"
   
 
diff --git a/Curry/Base/Ident.lhs b/Curry/Base/Ident.lhs
--- a/Curry/Base/Ident.lhs
+++ b/Curry/Base/Ident.lhs
@@ -133,7 +133,7 @@
 > mkIdent x = Ident NoPos x 0
 
 > renameIdent :: Ident -> Int -> Ident
-> renameIdent (Ident p x _) n = Ident p x n
+> renameIdent id n = id { uniqueId = n }
 
 
 > unRenameIdent :: Ident -> Ident
@@ -192,7 +192,7 @@
 > updQualIdent f g (QualIdent m x) = QualIdent (liftM f m) (g x)
 
 > addRef :: SrcRef -> QualIdent -> QualIdent
-> addRef r = updQualIdent id (addRefId r)
+> addRef = updQualIdent id . addRefId
 
 > addRefId :: SrcRef -> Ident -> Ident
 > addRefId = addPositionIdent . AST
@@ -280,7 +280,7 @@
 > fpSelectorId n = Ident NoPos (fpSelExt ++ show n) 0
 
 > isFpSelectorId :: Ident -> Bool
-> isFpSelectorId f = any (fpSelExt `isPrefixOf`) (tails (name f))
+> isFpSelectorId = any (fpSelExt `isPrefixOf`) . tails . name
 
 > isQualFpSelectorId :: QualIdent -> Bool
 > isQualFpSelectorId = isFpSelectorId . unqualify
@@ -291,7 +291,7 @@
 
 > qualRecSelectorId :: ModuleIdent -> QualIdent -> Ident -> QualIdent
 > qualRecSelectorId m r l = qualifyWith m' (recSelectorId r l)
->   where m' = (fromMaybe m (fst (splitQualIdent r)))
+>   where m' = fromMaybe m (fst (splitQualIdent r))
 
 > recUpdateId :: QualIdent -> Ident -> Ident
 > recUpdateId r l = 
@@ -299,7 +299,7 @@
 
 > qualRecUpdateId :: ModuleIdent -> QualIdent -> Ident -> QualIdent
 > qualRecUpdateId m r l = qualifyWith m' (recUpdateId r l)
->   where m' = (fromMaybe m (fst (splitQualIdent r)))
+>   where m' = fromMaybe m (fst (splitQualIdent r))
 
 > recordExtId :: Ident -> Ident
 > recordExtId r = mkIdent (recordExt ++ name r)
diff --git a/Curry/Base/MessageMonad.hs b/Curry/Base/MessageMonad.hs
--- a/Curry/Base/MessageMonad.hs
+++ b/Curry/Base/MessageMonad.hs
@@ -53,7 +53,7 @@
 
 
 failWithAt :: (MonadError WarnMsg m) => Position -> String -> m a
-failWithAt p s  = throwError (WarnMsg (Just p) s)
+failWithAt p = throwError . WarnMsg (Just p)
 
 
 warnMessage :: (MonadWriter [WarnMsg] m) => String -> m ()
diff --git a/Curry/ExtendedFlat/CurryArithmetics.hs b/Curry/ExtendedFlat/CurryArithmetics.hs
new file mode 100644
--- /dev/null
+++ b/Curry/ExtendedFlat/CurryArithmetics.hs
@@ -0,0 +1,74 @@
+{-
+  In Curry, Integers are encoded as binary values,
+  being represented by constructor terms.
+
+  (c) Holger Siegel 2009
+-}
+module Curry.ExtendedFlat.CurryArithmetics
+    (CurryInt(..), CurryNat(..),
+     trNat, trInt,
+     toCurryInt, toIntExpression,
+    ) where
+
+import Curry.ExtendedFlat.Type
+
+
+data CurryInt = Neg CurryNat | Zero | Pos CurryNat
+data CurryNat = IHi | O CurryNat | I CurryNat
+
+
+trNat :: Integral n =>
+         a -> (a -> a) -> (a -> a) ->
+         n -> a
+trNat h o i = go
+    where go n | n `mod` 2 == 0 = o (go m)
+               | m == 0         = h
+               | otherwise      = i (go m)
+              where m = n `div` 2
+
+
+trInt :: Integral n =>
+         (nat -> t) -> t -> (nat -> t) ->
+         nat -> (nat -> nat) -> (nat -> nat) ->
+         n -> t
+trInt n z p h o i = go
+    where go x = case compare x 0 of
+                   LT -> n (trNat h o i (negate x))
+                   EQ -> z
+                   GT -> p (trNat h o i x)
+
+
+toCurryInt :: Integral a => a -> CurryInt
+toCurryInt = trInt Neg Zero Pos IHi O I
+
+
+toIntExpression :: Integral a => a -> Expr
+toIntExpression = trInt neg_ zero_ pos_ iHi_ o_ i_
+
+
+zero_, iHi_ :: Expr
+pos_, neg_, o_, i_ :: Expr -> Expr
+
+zero_  = prelCons tInt0 "Zero" []
+pos_ n = prelCons tInt1 "Pos" [n]
+neg_ n = prelCons tInt1 "Neg" [n]
+
+iHi_ = prelCons tNat0 "IHi" []
+o_ n = prelCons tNat1 "O" [n]
+i_ n = prelCons tNat1 "I" [n]
+
+
+tInt0, tInt1, tNat0, tNat1 :: TypeExpr
+tInt0 = prelType "Int"
+tInt1 = FuncType tInt0 tInt0
+
+tNat0 = prelType "Nat"
+tNat1 = FuncType tNat0 tNat0
+
+
+prelType :: String -> TypeExpr
+prelType s = TCons (mkQName ("Prelude", s)) []
+
+
+prelCons :: TypeExpr -> String -> [Expr] -> Expr
+prelCons t = Comb ConsCall . QName Nothing (Just t) "Prelude"
diff --git a/Curry/ExtendedFlat/EraseTypes.hs b/Curry/ExtendedFlat/EraseTypes.hs
new file mode 100644
--- /dev/null
+++ b/Curry/ExtendedFlat/EraseTypes.hs
@@ -0,0 +1,88 @@
+{-
+  Erases type annotations an ExtendedFlat module.
+  In functions, it preserves annotations that contain
+  free type variables, i.e. type variables  which do
+  not occur in the function's type signature.
+
+  In the remaining type annotations, free type variables
+  are replaced by the unit type ().
+
+  (c) 2009, Holger Siegel.
+-}
+
+module Curry.ExtendedFlat.EraseTypes(eraseTypes) where
+
+import Control.Monad.Reader
+import qualified Data.Set as Set
+
+import Curry.ExtendedFlat.Type
+import Curry.ExtendedFlat.Goodies
+import Curry.ExtendedFlat.MonadicGoodies
+
+
+-- FIXME the use of lists is not very efficient,
+-- but since the number of type variables is relatively
+-- small, we stick with that for now.
+type TVarSet = [TVarIndex]
+
+
+eraseTypes :: Prog -> Prog
+eraseTypes = updProg id id id (map eraseTypesInFunc) id
+
+
+eraseTypesInFunc :: FuncDecl -> FuncDecl
+eraseTypesInFunc (Func qname arity visty funtype rule)
+    = Func qname arity visty funtype rule'
+    where rule' = eraseTypesInRule (allTVars funtype) rule
+
+
+eraseTypesInRule :: TVarSet -> Rule -> Rule
+eraseTypesInRule sigtvars r@(External _) = r
+eraseTypesInRule sigtvars (Rule vars expr)
+    = Rule (map (eraseTypesInVar sigtvars) vars) (eraseTypesInExpr sigtvars expr)
+
+
+eraseTypesInExpr :: TVarSet -> Expr -> Expr
+eraseTypesInExpr sigtvars 
+    = rnmAllVars (eraseTypesInVar sigtvars) .
+      updQNames (eraseTypesInQName sigtvars)
+
+
+eraseTypesInVar :: TVarSet -> VarIndex -> VarIndex
+eraseTypesInVar sigtvars v
+    = v {typeofVar = vt' }
+    where 
+      vt = typeofVar v
+      usedtvars = maybe [] allTVars vt
+      vt' | all (`elem` sigtvars) usedtvars
+              = Nothing
+          | otherwise
+              = fmap (replaceFreeTypesWithEmptyTuple sigtvars) vt
+
+
+eraseTypesInQName :: TVarSet -> QName -> QName
+eraseTypesInQName sigtvars v
+     = v {typeofQName = qt' }
+    where 
+      qt = typeofQName v
+      usedtvars = maybe [] allTVars qt
+      qt' | all (`elem` sigtvars) usedtvars
+              = Nothing
+          | otherwise
+              = fmap (replaceFreeTypesWithEmptyTuple sigtvars) qt
+                     
+
+allTVars :: TypeExpr -> [TVarIndex]
+allTVars t = go t []
+    where
+      go (TVar v)       is = v : is
+      go (FuncType x e) is = go x (go e is)
+      go (TCons _ ts)   is = foldr go is ts
+
+
+replaceFreeTypesWithEmptyTuple :: TVarSet -> TypeExpr -> TypeExpr
+replaceFreeTypesWithEmptyTuple usedtvars = updTVars foo
+    where 
+      foo tidx
+          | tidx `elem` usedtvars = TVar tidx
+          | otherwise = TCons (mkQName ("Prelude", "()")) []
diff --git a/Curry/ExtendedFlat/Goodies.hs b/Curry/ExtendedFlat/Goodies.hs
--- a/Curry/ExtendedFlat/Goodies.hs
+++ b/Curry/ExtendedFlat/Goodies.hs
@@ -17,6 +17,7 @@
 
 module Curry.ExtendedFlat.Goodies where
 
+import Control.Arrow(first, second)
 import Control.Monad(mplus, msum)
 import Data.List
 
@@ -299,15 +300,15 @@
 
 --- is type expression a type variable?
 isTVar :: TypeExpr -> Bool
-isTVar = trTypeExpr (\_ -> True) (\_ _ -> False) (\_ _ -> False)
+isTVar = trTypeExpr (const True) (\_ _ -> False) (\_ _ -> False)
 
 --- is type declaration a constructed type?
 isTCons :: TypeExpr -> Bool
-isTCons = trTypeExpr (\_ -> False) (\_ _ -> True) (\_ _ -> False)
+isTCons = trTypeExpr (const False) (\_ _ -> True) (\_ _ -> False)
 
 --- is type declaration a functional type?
 isFuncType :: TypeExpr -> Bool
-isFuncType = trTypeExpr (\_ -> False) (\_ _ -> False) (\_ _ -> True)
+isFuncType = trTypeExpr (const False) (\_ _ -> False) (\_ _ -> True)
 
 -- Update Operations
 
@@ -343,11 +344,11 @@
 
 --- rename variables in type expression
 rnmAllVarsInTypeExpr :: (TVarIndex -> TVarIndex) -> TypeExpr -> TypeExpr
-rnmAllVarsInTypeExpr f = updTVars (TVar . f)
+rnmAllVarsInTypeExpr = updTVars . (TVar .)
 
 --- update all qualified names in type expression
 updQNamesInTypeExpr :: (QName -> QName) -> TypeExpr -> TypeExpr
-updQNamesInTypeExpr f = updTCons (\name args -> TCons (f name) args)
+updQNamesInTypeExpr f = updTCons (TCons . f)
 
 -- OpDecl --------------------------------------------------------------------
 
@@ -520,7 +521,7 @@
 
 --- is rule external?
 isRuleExternal :: Rule -> Bool
-isRuleExternal = trRule (\_ _ -> False) (\_ -> True)
+isRuleExternal = trRule (\_ _ -> False) (const True)
 
 -- Update Operations
 
@@ -531,7 +532,7 @@
 updRule fa fe fs = trRule rule ext
  where
   rule as e = Rule (fa as) (fe e)
-  ext s = External (fs s)
+  ext = External . fs
 
 --- update rules arguments
 updRuleArgs :: Update Rule [VarIndex]
@@ -543,13 +544,13 @@
 
 --- update rules external declaration
 updRuleExtDecl :: Update Rule String
-updRuleExtDecl f = updRule id id f
+updRuleExtDecl = updRule id id
 
 -- Auxiliary Functions
 
 --- get variable names in a functions rule
 allVarsInRule :: Rule -> [VarIndex]
-allVarsInRule = trRule (\args body -> args ++ allVars body) (\_ -> [])
+allVarsInRule = trRule (\args body -> args ++ allVars body) (const [])
 
 --- rename all variables in rule
 rnmAllVarsInRule :: Update Rule VarIndex
@@ -572,19 +573,19 @@
 
 --- is type of combination FuncCall?
 isCombTypeFuncCall :: CombType -> Bool
-isCombTypeFuncCall = trCombType True (\_ -> False) False (\_ -> False)
+isCombTypeFuncCall = trCombType True (const False) False (const False)
 
 --- is type of combination FuncPartCall?
 isCombTypeFuncPartCall :: CombType -> Bool
-isCombTypeFuncPartCall = trCombType False (\_ -> True) False (\_ -> False)
+isCombTypeFuncPartCall = trCombType False (const True) False (const False)
 
 --- is type of combination ConsCall?
 isCombTypeConsCall :: CombType -> Bool
-isCombTypeConsCall = trCombType False (\_ -> False) True (\_ -> False)
+isCombTypeConsCall = trCombType False (const False) True (const False)
 
 --- is type of combination ConsPartCall?
 isCombTypeConsPartCall :: CombType -> Bool
-isCombTypeConsPartCall = trCombType False (\_ -> False) False (\_ -> True)
+isCombTypeConsPartCall = trCombType False (const False) False (const True)
 
 -- Auxiliary Functions
 
@@ -712,7 +713,7 @@
   = comb ct name (map (trExpr var lit comb lt fr oR cas branch) args)
 
 trExpr var lit comb lt fr oR cas branch (Let bs e)
-  = lt (map (\ (n,e) -> (n,f e)) bs) (f e)
+  = lt (map (second f) bs) (f e)
  where
   f = trExpr var lit comb lt fr oR cas branch
 
@@ -760,7 +761,7 @@
 
 --- update all case branches in given expression
 updBranches :: (Pattern -> Expr -> BranchExpr) -> Expr -> Expr
-updBranches branch = trExpr Var Lit Comb Let Free Or Case branch
+updBranches = trExpr Var Lit Comb Let Free Or Case
 
 -- Auxiliary Functions
 
@@ -792,10 +793,10 @@
 allVars expr = trExpr (:) (const id) comb lt fr (.) cas branch expr []
  where
   comb _ _ = foldr (.) id
-  lt bs e = e . foldr (.) id (map (\ (n,ns) -> (n:) . ns) bs)
-  fr vs e = (vs++) . e
+  lt bs = (. foldr (.) id (map (\ (n,ns) -> (n:) . ns) bs))
+  fr    = (.) . (++)
   cas _ _ e bs = e . foldr (.) id bs
-  branch pat e = ((args pat)++) . e
+  branch = (.) . (++) . args
   args pat | isConsPattern pat = patArgs pat
            | otherwise = []
 
@@ -803,14 +804,14 @@
 rnmAllVars :: Update Expr VarIndex
 rnmAllVars f = trExpr (Var . f) Lit Comb lt (Free . map f) Or Case branch
  where
-   lt = Let . map (\ (n,e) -> (f n,e))
+   lt = Let . map (first f)
    branch = Branch . updPatArgs (map f)
 
 --- update all qualified names in expression
 updQNames :: Update Expr QName
 updQNames f = trExpr Var Lit comb Let Free Or Case (Branch . updPatCons f)
  where
-  comb ct name args = Comb ct (f name) args
+  comb ct = Comb ct . f
 
 -- BranchExpr ----------------------------------------------------------------
 
@@ -869,7 +870,7 @@
 
 --- is pattern a constructor pattern?
 isConsPattern :: Pattern -> Bool
-isConsPattern = trPattern (\_ _ -> True) (\_ -> False)
+isConsPattern = trPattern (\_ _ -> True) (const False)
 
 -- Update Operations
 
@@ -880,7 +881,7 @@
 updPattern fn fa fl = trPattern pattern lpattern
  where
   pattern name args = Pattern (fn name) (fa args)
-  lpattern l = LPattern (fl l)
+  lpattern = LPattern . fl
 
 --- update constructors name of pattern
 updPatCons :: (QName -> QName) -> Pattern -> Pattern
@@ -892,7 +893,7 @@
 
 --- update literal of pattern
 updPatLiteral :: (Literal -> Literal) -> Pattern -> Pattern
-updPatLiteral f = updPattern id id f
+updPatLiteral = updPattern id id
 
 -- Auxiliary Functions
 
@@ -901,25 +902,27 @@
 patExpr = trPattern (\ name -> Comb ConsCall name . map Var) Lit
 
 
--- get the type of an expression
+-- |  Get the type of an expression.
 -- (Will only succeed if all VarIndices and QNames contain the
--- required type information.)
+-- required type information. Make sure that the expression is processed by
+-- Curry.ExtendedFlat.TypeInference.adjustTypeInfo.)
 typeofExpr :: Expr -> Maybe TypeExpr
 typeofExpr expr 
     = case expr of
         Var vi        -> typeofVar vi
         Lit l         -> Just (typeofLiteral l)
-        Comb _  qn as -> fmap (typeofApp as) (typeofQName qn)
+        Comb _  qn as -> typeofQName qn >>= typeofApp as
         Free _ e      -> typeofExpr e
         Let _ e       -> typeofExpr e
         Or e1 e2      -> typeofExpr e1 `mplus` typeofExpr e2
         Case _ _ _ bs -> msum (map (typeofExpr . branchExpr) bs)
     where 
-      typeofApp []     t              = t
-      typeofApp (_:as) (FuncType _ t) = typeofApp as t
-      typeofApp (_:_)  (TVar _)       = ierr
-      typeofApp (_:_)  (TCons _ _)    = ierr
-      ierr = error $ "internal error in typeofExpr: FuncType expected"
+      typeofApp :: [a] -> TypeExpr -> Maybe TypeExpr
+      typeofApp []      t              = Just t
+      typeofApp (_:as)  (FuncType _ t) = typeofApp as t
+      typeofApp (_:_)   (TVar _)       = Nothing
+      typeofApp a@(_:_) (TCons _ _)    = Nothing
+      -- ierr = error "internal error in typeofExpr: FuncType expected"
 
 
 typeofLiteral :: Literal -> TypeExpr
diff --git a/Curry/ExtendedFlat/LiftLetrec.hs b/Curry/ExtendedFlat/LiftLetrec.hs
--- a/Curry/ExtendedFlat/LiftLetrec.hs
+++ b/Curry/ExtendedFlat/LiftLetrec.hs
@@ -73,7 +73,6 @@
     = do name <- newGlobalName t
          st <- get
          let fcall = (Comb FuncCall name (map Var fv))
-         -- FIXME Typ der Funktion muss irgendwie ermittelt werden :(
          let fdecl = Func name (length fv) Private (fromMaybe (TVar 0) t) (Rule fv (Let [(v,fcall)] rhs))
          put st { lifted = Map.insert name fdecl (lifted st),
                   globals = Set.insert name (globals st)
diff --git a/Curry/ExtendedFlat/Type.hs b/Curry/ExtendedFlat/Type.hs
--- a/Curry/ExtendedFlat/Type.hs
+++ b/Curry/ExtendedFlat/Type.hs
@@ -421,7 +421,6 @@
 writeExtendedFlat inHiddenSubdir filename prog =
   writeModule inHiddenSubdir (extFlatName filename) (showFlatCurry' True prog)
 
-
 showFlatCurry' :: Bool -> Prog -> String
 showFlatCurry' b x = gshowsPrec b False x ""
 
diff --git a/Curry/ExtendedFlat/TypeInference.hs b/Curry/ExtendedFlat/TypeInference.hs
--- a/Curry/ExtendedFlat/TypeInference.hs
+++ b/Curry/ExtendedFlat/TypeInference.hs
@@ -16,8 +16,7 @@
       adjustTypeInfo,
       labelVarsWithTypes,
       uniqueTypeIndices,
-      genEquations,
-      elimFreeTypes
+      genEquations
     ) where
 
 import Debug.Trace
@@ -38,8 +37,7 @@
 --   of a declaration, the polymorphic type variables in its
 --   type label are replaced by concrete types.
 adjustTypeInfo :: Prog -> Prog
-adjustTypeInfo = -- elimFreeTypes .
-                 genEquations . 
+adjustTypeInfo = genEquations . 
                  uniqueTypeIndices .
                  labelVarsWithTypes
 
@@ -56,11 +54,11 @@
 prettyAllEqns = render . prettyEqns
     where
       prettyEqn ::(TVarIndex, TypeExpr)  -> Doc
-      prettyEqn (l, r) = (char 't' <> int l <+> text "->" <+> prettyType r)
+      prettyEqn (l, r) = char 't' <> int l <+> text "->" <+> prettyType r
 
       prettyEqns ((m,l), t, eqns)
           = text m <> char '.' <> text l <+> text "::" <+> prettyType t <> char ':'
-            $$ (nest 5 (vcat (map prettyEqn eqns)))
+            $$ nest 5 (vcat (map prettyEqn eqns))
 
 
 postOrderExpr :: Monad m => (Expr -> m Expr) -> Expr -> m Expr
@@ -105,6 +103,8 @@
 -- ----------------------------------------------------------------------
 -- ----------------------------------------------------------------------
 
+type TDictM = ReaderT TypeMap (State Int)
+
 -- | All identifiers that do not have type annotations are
 --   labelled with new type variables
 labelVarsWithTypes :: Prog -> Prog
@@ -119,18 +119,19 @@
                 argTypes = [ (vi, t) | VarIndex (Just t) vi <- vs ]
             in Func qn arity visty te (Rule vs expr')
 
-      po :: Expr -> ReaderT TypeMap (State Int) Expr
+      po :: Expr -> TDictM Expr
       -- type information from vi is superseded by type information
       -- from the map. This is okay in the current context, but for
       -- general type inference this would result in loss of information.
       -- (Fix by unifying both types in a later version)
       po e@(Var vi)
           = do vt <- asks (IntMap.lookup $ idxOf vi)
-               case vt of
-                 Just t -> return (Var vi { typeofVar = Just t })
-                 Nothing -> case typeofVar vi of
-                              Nothing -> error $ "no type for var " ++ show e
-                              _ -> liftM Var (poVarIndex vi)
+               trace' ("labelVarsWithTypes " ++ show e ++" :: "++ show vt)(
+                                                                         case vt of
+                                                                           Just t -> return (Var vi { typeofVar = Just t })
+                                                                           Nothing -> case typeofVar vi of
+                                                                                        Nothing -> error $ "no type for var " ++ show e
+                                                                                        _ -> liftM Var (poVarIndex vi))
       po e@(Lit _)
           = return e
       po (Comb t n es)
@@ -153,6 +154,8 @@
           = do e' <- po e
                bs' <- mapM poBranch bs
                return (Case p t e' bs')
+
+      poBranch :: BranchExpr -> TDictM BranchExpr
       poBranch (Branch (Pattern qn vs) rhs) 
           = do qn' <- poQName qn
                vs' <- mapM poVarIndex vs
@@ -160,18 +163,21 @@
                               return (Branch (Pattern qn' vs') rhs'))
       poBranch (Branch (LPattern l) e) 
           = do rhs' <- po e
-               return (Branch (LPattern l) e)
+               return (Branch (LPattern l) rhs')
+
+      poVarIndex :: VarIndex -> TDictM VarIndex
       poVarIndex vi
           = do t <- maybe (lift$freshTVar) return . typeofVar $ vi
                return vi{typeofVar = Just t }
 
+      poQName :: QName -> TDictM QName
       poQName qn
           = do t <- maybe (lift$freshTVar) 
                         return . typeofQName $ qn
                return qn{typeofQName = Just t }
 
       withVS :: MonadReader TypeMap m => [VarIndex] -> m a -> m a
-      withVS vs action = local (\ m -> foldr (\ v -> IntMap.insert (idxOf v) (fromJust $ typeofVar v)) m vs) action
+      withVS vs = local (\ m -> foldr (\ v -> IntMap.insert (idxOf v) (fromJust $ typeofVar v)) m vs)
 
 -- ----------------------------------------------------------------------
 -- ----------------------------------------------------------------------
@@ -183,7 +189,7 @@
 uniqueTypeIndices = updProgFuncs (map updateFunc)
     where
       updateFunc func = let firstfree = maxFuncTV func + 1
-                        in (updFuncRule (trRule (ruleFoo firstfree) External)) func
+                        in updFuncRule (trRule (ruleFoo firstfree) External) func
       ruleFoo firstfree args expr
           = let expr' = evalState (postOrderExpr relabelTypes expr) firstfree
             in  Rule args expr'
@@ -255,7 +261,8 @@
                tqn =:= foldr FuncType resultType argTypes
                return resultType
 
-      letEqn _ e = e
+      letEqn :: ([(VarIndex, EqnMonad TypeExpr)] -> EqnMonad TypeExpr -> EqnMonad TypeExpr)
+      letEqn bs = (mapM_ bindEqn bs >>)
 
       frEqn _ e = e
 
@@ -263,27 +270,37 @@
                      r' <- r
                      l' =:= r'
 
-      casEqn :: SrcRef -> CaseType -> EqnMonad TypeExpr -> [(Pattern, EqnMonad TypeExpr)] -> EqnMonad TypeExpr
+      casEqn :: SrcRef -> CaseType -> EqnMonad TypeExpr -> [EqnMonad (Pattern, TypeExpr)] -> EqnMonad TypeExpr
       casEqn _ _ scr [] = scr >> (lift$freshTVar)
       casEqn _ _ scr ps = do scrt <- scr
                              -- unify patterns with scrutinee
-                             mapM_ (unifLhs scrt) ps
+                             branches <- sequence ps
+                             let pats = map fst branches
+                             let (p:ps') = map snd branches
+                             mapM_ (unifLhs scrt) pats
+                             -- foldM (\l r -> unifLhs scrt r >>= (=:= l)) scrt pats
                              -- unify right hand sides
-                             (p:ps') <- sequence $ map snd ps
                              foldM (=:=) p ps'
 
-      unifLhs scrt (LPattern lit, _)
+      unifLhs scrt (LPattern lit)
           = typeofLiteral lit =:= scrt
-      unifLhs scrt (Pattern qn vs, _)
+      unifLhs scrt (Pattern qn vs)
           = do qnt <- qnType qn
+              -- FIXME: Variablentypen in Map eintragen!!!
                argTypes <- mapM varIndexType vs
                qnt =:= foldr FuncType scrt argTypes
 
 
-      branchEqn :: Pattern -> EqnMonad TypeExpr -> (Pattern, EqnMonad TypeExpr)
-      branchEqn p e = (p, e)
+      branchEqn :: Pattern -> EqnMonad TypeExpr -> EqnMonad (Pattern, TypeExpr)
+      branchEqn p e = do trhs <- e
+                         return (p, trhs)
 
+      bindEqn :: (VarIndex, EqnMonad TypeExpr) -> EqnMonad TypeExpr
+      bindEqn (vi, rhs) = do vit <- varIndexType vi
+                             rvi <- rhs
+                             vit =:= rvi
 
+
 unify :: TypeExpr -> TypeExpr -> TypeMap -> TypeMap
 -- t =:= u = return t
 
@@ -328,31 +345,7 @@
                modify succ
                return (TVar nextIdx)
 
----------------------------------------------------------------------
 
--- | Type variables that occur in the right hand side of a declaration
---   but not in its type signature are replaced by the unit type ().
---   This function requires that proper type information has been made
---   available by function @adjustTypeInfo@
-
-elimFreeTypes :: Prog -> Prog
-elimFreeTypes = updProgFuncs updateFunc
-    where 
-      updateFunc = map (trFunc foo)
-      foo qn arity visty te r@(External _) = Func qn arity visty te r
-      foo qn arity visty te r@(Rule vs expr) 
-          = let tvs = tvars te
-                tvars (TVar vi) = [vi]
-                tvars (FuncType t1 t2) = tvars t1 ++ tvars t2
-                tvars (TCons _ ts) = concatMap tvars ts
-                tfoo t@(TVar vi)
-                    | vi `elem` tvs = t
-                    | otherwise = TCons (mkQName ("Prelude", "()")) []
-                tfoo (FuncType t1 t2) = FuncType (tfoo t1) (tfoo t2)
-                tfoo (TCons qn ts) = TCons qn (map tfoo ts)
-            in Func qn arity visty te (modifyType tfoo (Rule vs expr))
-
-
 ---------------------------------------------------------------------
 
 maxFuncTV = trFunc (\qn _ _ te r -> max (maxQNameTV qn) (max (maxTypeTV te) (maxRuleTV r)))
@@ -391,7 +384,7 @@
 
 -- boilerplate
 specInRule :: TypeMap -> Rule -> Rule
-specInRule tm = modifyType (specialiseType tm)
+specInRule = modifyType . specialiseType
 
 
 
@@ -400,16 +393,15 @@
 modifyType f = updRule (map specInVarIndex) specInExpr id
     where specInExpr
               = trExpr var Lit comb letexp free Or Case alt
-          var vi
-              = Var (specInVarIndex vi)
-          comb ct qn as
-              = Comb ct (specInQName qn) as
-          letexp bs e
-              = Let (map specInBind bs) e
-          free vis e
-              = Free (map specInVarIndex vis) e
-          alt p e
-              = Branch (specInPattern p) e
+          var = Var . specInVarIndex
+          comb ct 
+              = Comb ct . specInQName
+          letexp
+              = Let . map specInBind
+          free
+              = Free . map specInVarIndex
+          alt
+              = Branch . specInPattern
 
           specInBind (vi, e)
               = (specInVarIndex vi, e)
diff --git a/Curry/ExtendedFlat/UnMutual.hs b/Curry/ExtendedFlat/UnMutual.hs
--- a/Curry/ExtendedFlat/UnMutual.hs
+++ b/Curry/ExtendedFlat/UnMutual.hs
@@ -67,9 +67,6 @@
 -- Some self-explaining helper functions:
 
 
--- FIXME rename, wenn x in (fvs e1) !
--- immer rename wg. Shadowing
--- (siehe Test.curry)
 nonrecLet :: VarIndex -> Expr -> Expr -> UnMutualMonad Expr
 nonrecLet x e1 e2
     | x `elem` allVars e1 
diff --git a/Curry/Files/PathUtils.hs b/Curry/Files/PathUtils.hs
--- a/Curry/Files/PathUtils.hs
+++ b/Curry/Files/PathUtils.hs
@@ -19,7 +19,7 @@
 import System.Directory
 import System.Time (ClockTime)
 
-import Control.Monad (unless)
+import Control.Monad (unless, liftM)
 
 import Curry.Base.Ident
 import Curry.Files.Filenames
@@ -107,7 +107,7 @@
 
 maybeReadModule :: FilePath -> IO (Maybe String)
 maybeReadModule filename = 
-  catch (readModule filename >>= return . Just) (\_ -> return Nothing)
+  catch (liftM Just (readModule filename)) (\_ -> return Nothing)
 
 doesModuleExist :: FilePath -> IO Bool
 doesModuleExist = onExistingFileDo doesFileExist
diff --git a/Curry/FlatCurry/Tools.hs b/Curry/FlatCurry/Tools.hs
--- a/Curry/FlatCurry/Tools.hs
+++ b/Curry/FlatCurry/Tools.hs
@@ -789,7 +789,7 @@
 
 --- flatten pattern variables
 allVarsPat :: Pattern -> [Int]
-allVarsPat = maybe [] id . patArgs
+allVarsPat = fromMaybe [] . patArgs
 
 -- opDecls ------------------------------
 
diff --git a/Curry/FlatCurry/Type.hs b/Curry/FlatCurry/Type.hs
--- a/Curry/FlatCurry/Type.hs
+++ b/Curry/FlatCurry/Type.hs
@@ -341,8 +341,8 @@
 showFlatCurry (Prog mname imps types funcs ops) =
   "Prog "++show mname++"\n "++
   show imps ++"\n ["++
-  concat (intersperse ",\n  " (map (\t->show t) types)) ++"]\n ["++
-  concat (intersperse ",\n  " (map (\f->show f) funcs)) ++"]\n "++
+  concat (intersperse ",\n  " (map show types)) ++"]\n ["++
+  concat (intersperse ",\n  " (map show funcs)) ++"]\n "++
   show ops ++"\n"
   
 
diff --git a/curry-base.cabal b/curry-base.cabal
--- a/curry-base.cabal
+++ b/curry-base.cabal
@@ -1,5 +1,5 @@
 Name:          curry-base
-Version:       0.2.7
+Version:       0.2.8
 Cabal-Version: >= 1.6
 Synopsis:      Functions for manipulating Curry programs
 Description:   This package serves as a foundation for Curry compilers. it defines the intermediate
@@ -28,6 +28,8 @@
     Curry.ExtendedFlat.MonadicGoodies
     Curry.ExtendedFlat.UnMutual
     Curry.ExtendedFlat.LiftLetrec
+    Curry.ExtendedFlat.EraseTypes
+    Curry.ExtendedFlat.CurryArithmetics
     Curry.FlatCurry.Type
     Curry.FlatCurry.Goodies
     Curry.FlatCurry.Tools