--- a/Nominal/Ex/LF.thy	Wed Aug 25 23:16:42 2010 +0800
+++ b/Nominal/Ex/LF.thy	Thu Aug 26 02:08:00 2010 +0800
@@ -2,7 +2,7 @@
 imports "../NewParser"
 begin
 
-declare [[STEPS = 9]]
+declare [[STEPS = 20]]
 
 atom_decl name
 atom_decl ident
@@ -13,17 +13,14 @@
 and ty =
     TConst "ident"
   | TApp "ty" "trm"
-  | TPi "ty" n::"name" t::"ty"   bind n in t
+  | TPi "ty" n::"name" ty::"ty"   bind n in ty
 and trm =
     Const "ident"
   | Var "name"
   | App "trm" "trm"
   | Lam "ty" n::"name" t::"trm"  bind n in t
 
-thm kind_ty_trm.supp
-
-
-
+(*thm kind_ty_trm.supp*)
 
 
 end