--- a/Nominal/Ex/LetRec.thy	Thu Aug 26 02:08:00 2010 +0800
+++ b/Nominal/Ex/LetRec.thy	Fri Aug 27 02:03:52 2010 +0800
@@ -2,22 +2,20 @@
 imports "../NewParser"
 begin
 
-declare [[STEPS = 14]]
-
 atom_decl name
 
 nominal_datatype let_rec:
- lam =
+ trm =
   Var "name"
-| App "lam" "lam"
-| Lam x::"name" t::"lam"     bind (set) x in t
-| Let_Rec bp::"bp" t::"lam"  bind (set) "bi bp" in bp t
+| App "trm" "trm"
+| Lam x::"name" t::"trm"     bind (set) x in t
+| Let_Rec bp::"bp" t::"trm"  bind (set) "bn bp" in bp t
 and bp =
-  Bp "name" "lam"
+  Bp "name" "trm"
 binder
-  bi::"bp \<Rightarrow> atom set"
+  bn::"bp \<Rightarrow> atom set"
 where
-  "bi (Bp x t) = {atom x}"
+  "bn (Bp x t) = {atom x}"
 
 thm let_rec.distinct
 thm let_rec.induct