diff --git a/src/GF/Compile/CheckGrammar.hs b/src/GF/Compile/CheckGrammar.hs
index f8a1911c9..fb42bd17e 100644
--- a/src/GF/Compile/CheckGrammar.hs
+++ b/src/GF/Compile/CheckGrammar.hs
@@ -5,9 +5,9 @@
 -- Stability   : (stable)
 -- Portability : (portable)
 --
--- > CVS $Date: 2005/06/22 08:52:02 $ 
+-- > CVS $Date: 2005/10/02 20:50:19 $ 
 -- > CVS $Author: aarne $
--- > CVS $Revision: 1.28 $
+-- > CVS $Revision: 1.29 $
 --
 -- AR 4\/12\/1999 -- 1\/4\/2000 -- 8\/9\/2001 -- 15\/5\/2002 -- 27\/11\/2002 -- 18\/6\/2003
 --
@@ -93,18 +93,25 @@ checkAbsInfo st m (c,info) = do
      checkContext st cont ---- also cstrs
    AbsFun (Yes typ0) md -> do
     typ <- compAbsTyp [] typ0   -- to calculate let definitions
-    mkCheck "function" $
-       checkTyp st typ ++ 
-       case md of
-         Yes d ->  checkEquation st (m,c) d
-         _ -> []
-    return $ (c,AbsFun (Yes typ) md)
+    mkCheck "type of function" $ checkTyp st typ 
+    md' <- case md of
+       Yes d -> do
+         let d' = elimTables d
+         mkCheckWarn "definition of function" $ checkEquation st (m,c) d'
+         return $ Yes d'
+       _ -> return md
+    return $ (c,AbsFun (Yes typ) md')
    _ -> return (c,info)
  where
    mkCheck cat ss = case ss of
      [] -> return (c,info)
      ["[]"] -> return (c,info) ----
      _  -> checkErr $ prtBad (unlines ss ++++ "in" +++ cat) c
+   ---- temporary solution when tc of defs is incomplete
+   mkCheckWarn cat ss = case ss of
+     [] -> return (c,info)
+     ["[]"] -> return (c,info) ----
+     _  -> checkWarn (unlines ss ++++ "in" +++ cat +++ prt c) >> return (c,info)
    compAbsTyp g t = case t of
      Vr x -> maybe (fail ("no value given to variable" +++ prt x)) return $ lookup x g
      Let (x,(_,a)) b -> do
@@ -117,6 +124,16 @@ checkAbsInfo st m (c,info) = do
      Abs _ _ -> return t
      _ -> composOp (compAbsTyp g) t
 
+   elimTables e = case e of
+     S t a  -> elimSel (elimTables t) (elimTables a)
+     T _ cs -> Eqs [(elimPatt p, elimTables t) | (p,t) <- cs]
+     _ -> composSafeOp elimTables e
+   elimPatt p = case p of
+     PR lps -> map snd lps
+     _ -> [p]
+   elimSel t a = case a of
+     R fs -> mkApp t (map (snd . snd) fs)
+     _ -> mkApp t [a]
 
 checkCompleteGrammar :: SourceAbs -> SourceCnc -> Check (BinTree Ident Info)
 checkCompleteGrammar abs cnc = do
diff --git a/src/GF/Grammar/AbsCompute.hs b/src/GF/Grammar/AbsCompute.hs
index 35be020fa..b2139f90a 100644
--- a/src/GF/Grammar/AbsCompute.hs
+++ b/src/GF/Grammar/AbsCompute.hs
@@ -5,9 +5,9 @@
 -- Stability   : (stable)
 -- Portability : (portable)
 --
--- > CVS $Date: 2005/04/21 16:22:18 $ 
--- > CVS $Author: bringert $
--- > CVS $Revision: 1.7 $
+-- > CVS $Date: 2005/10/02 20:50:19 $ 
+-- > CVS $Author: aarne $
+-- > CVS $Revision: 1.8 $
 --
 -- computation in abstract syntax w.r.t. explicit definitions.
 --
@@ -72,12 +72,15 @@ computeAbsTermIn lookd xs e = errIn ("computing" +++ prt e) $ compt xs e where
        Ok (Just EData) -> Nothing  -- canonical --- should always be QC
        Ok md -> md
        _ -> Nothing
+     Eqs _ -> return t ---- for nested fn
      _ -> Nothing
 
 beta :: [Ident] -> Exp -> Exp
 beta vv c = case c of
   App (Abs x b) a -> beta vv $ substTerm vv [xvv] (beta (x:vv) b) 
                                                     where xvv = (x,beta vv a) 
+  Let (x,(_,a)) b -> beta vv $ substTerm vv [xvv] (beta (x:vv) b) 
+                                                    where xvv = (x,beta vv a) 
   App f         a -> let (a',f') = (beta vv a, beta vv f) in 
                      (if a'==a && f'==f then id else beta vv) $ App f' a'
   Prod x a b      -> Prod x (beta vv a) (beta (x:vv) b)
diff --git a/src/GF/Grammar/Macros.hs b/src/GF/Grammar/Macros.hs
index 746526c85..6f0ee3335 100644
--- a/src/GF/Grammar/Macros.hs
+++ b/src/GF/Grammar/Macros.hs
@@ -5,9 +5,9 @@
 -- Stability   : (stable)
 -- Portability : (portable)
 --
--- > CVS $Date: 2005/06/03 21:51:58 $ 
+-- > CVS $Date: 2005/10/02 20:50:19 $ 
 -- > CVS $Author: aarne $
--- > CVS $Revision: 1.22 $
+-- > CVS $Revision: 1.23 $
 --
 -- Macros for constructing and analysing source code terms.
 --
@@ -655,6 +655,10 @@ composOp co trm =
         i'  <- changeTableType co i
         return (TSh i' cc')
 
+   Eqs cc -> 
+     do cc' <- mapPairListM (co . snd) cc
+        return (Eqs cc')
+
    V ty vs ->
      do ty' <- co ty
         vs' <- mapM co vs
diff --git a/src/GF/Grammar/TC.hs b/src/GF/Grammar/TC.hs
index 5864c5af0..8cfe23408 100644
--- a/src/GF/Grammar/TC.hs
+++ b/src/GF/Grammar/TC.hs
@@ -5,9 +5,9 @@
 -- Stability   : (stable)
 -- Portability : (portable)
 --
--- > CVS $Date: 2005/09/15 16:22:02 $ 
+-- > CVS $Date: 2005/10/02 20:50:19 $ 
 -- > CVS $Author: aarne $
--- > CVS $Revision: 1.10 $
+-- > CVS $Revision: 1.11 $
 --
 -- Thierry Coquand's type checking algorithm that creates a trace
 -----------------------------------------------------------------------------
@@ -261,6 +261,9 @@ checkPatt th tenv exp val = do
    checkExpP tenv@(k,rho,gamma) exp val = case exp of
      Meta m -> return $ (AMeta m val, val, [])
      Vr x   -> return $ (AVr   x val, val, [])
+     EInt i -> return (AInt i, valAbsInt, [])
+     K s    -> return (AStr s, valAbsString, [])
+
      Q m c  -> do
        typ <- lookupConst th (m,c)
        return $ (ACn (m,c) typ, typ, [])
diff --git a/src/GF/Source/SourceToGrammar.hs b/src/GF/Source/SourceToGrammar.hs
index 4af60f1bf..563b9cc97 100644
--- a/src/GF/Source/SourceToGrammar.hs
+++ b/src/GF/Source/SourceToGrammar.hs
@@ -5,9 +5,9 @@
 -- Stability   : (stable)
 -- Portability : (portable)
 --
--- > CVS $Date: 2005/05/30 21:08:15 $ 
+-- > CVS $Date: 2005/10/02 20:50:19 $ 
 -- > CVS $Author: aarne $
--- > CVS $Revision: 1.26 $
+-- > CVS $Revision: 1.27 $
 --
 -- based on the skeleton Haskell module generated by the BNF converter
 -----------------------------------------------------------------------------
@@ -251,15 +251,20 @@ transCatDef x = case x of
 		       cont <- liftM concat $ mapM transDDecl ddecls
 		       return (i, G.AbsCat (yes cont) nope)
        listCat id ddecls size = do
-				let li = mkListId id
-				catd <- cat li ddecls
-				let cd = M.mkDecl (G.Vr id)
-				    lc = G.Vr li
-				    niltyp = M.mkProdSimple (genericReplicate size cd) lc
-				    nilfund = (mkBaseId id, G.AbsFun (yes niltyp) nope)
-				    constyp = M.mkProdSimple [cd, M.mkDecl lc] lc
-				    consfund = (mkConsId id, G.AbsFun (yes constyp) nope)
-				return [catd,nilfund,consfund]
+	 let 
+           li = mkListId id
+	 catd@(_,G.AbsCat (Yes cont0) _) <- cat li ddecls
+	 let
+           cont = [(mkId x i,ty) | (i,(x,ty)) <- zip [0..] cont0]
+           xs = map (G.Vr . fst) cont 
+           cd = M.mkDecl (M.mkApp (G.Vr id) xs)
+	   lc = M.mkApp (G.Vr li) xs
+	   niltyp = M.mkProdSimple (cont ++ genericReplicate size cd) lc
+	   nilfund = (mkBaseId id, G.AbsFun (yes niltyp) nope)
+	   constyp = M.mkProdSimple (cont ++ [cd, M.mkDecl lc]) lc
+	   consfund = (mkConsId id, G.AbsFun (yes constyp) nope)
+	 return [catd,nilfund,consfund]
+       mkId x i = if isWildIdent x then (mkIdent "x" i) else x
 
 transFunDef :: FunDef -> Err ([Ident], G.Type)
 transFunDef x = case x of