--- a/Nominal/Ex/LF.thy	Thu Jun 03 15:02:52 2010 +0200
+++ b/Nominal/Ex/LF.thy	Mon Jun 07 11:43:01 2010 +0200
@@ -2,21 +2,23 @@
 imports "../NewParser"
 begin
 
+declare [[STEPS = 9]]
+
 atom_decl name
 atom_decl ident
 
 nominal_datatype kind =
     Type
-  | KPi "ty" n::"name" k::"kind"  bind_set n in k
+  | KPi "ty" n::"name" k::"kind" bind n in k
 and ty =
     TConst "ident"
   | TApp "ty" "trm"
-  | TPi "ty" n::"name" t::"ty"    bind_set n in t
+  | TPi "ty" n::"name" t::"ty"   bind n in t
 and trm =
     Const "ident"
   | Var "name"
   | App "trm" "trm"
-  | Lam "ty" n::"name" t::"trm"   bind_set n in t
+  | Lam "ty" n::"name" t::"trm"  bind n in t
 
 thm kind_ty_trm.supp