--- a/Nominal/Ex/Ex1rec.thy	Tue May 04 16:33:38 2010 +0200
+++ b/Nominal/Ex/Ex1rec.thy	Tue May 04 16:39:12 2010 +0200
@@ -1,22 +1,22 @@
 theory Ex1rec
-imports "../Parser" 
+imports "../NewParser"
 begin
 
 atom_decl name
 
-ML {* val _ = recursive := true *}
-ML {* val _ = alpha_type := AlphaGen *}
+ML {* val _ = cheat_supp_eq := true *}
+
 nominal_datatype lam =
-  VAR "name"
-| APP "lam" "lam"
-| LAM x::"name" t::"lam"  bind x in t
-| LET bp::"bp" t::"lam"   bind "bi bp" in t
+  Var "name"
+| App "lam" "lam"
+| Lam x::"name" t::"lam"  bind_set x in t
+| Let bp::"bp" t::"lam"   bind_set "bi bp" in bp t
 and bp =
-  BP "name" "lam"
+  Bp "name" "lam"
 binder
   bi::"bp \<Rightarrow> atom set"
 where
-  "bi (BP x t) = {atom x}"
+  "bi (Bp x t) = {atom x}"
 
 thm lam_bp.fv
 thm lam_bp.eq_iff[no_vars]
@@ -25,8 +25,9 @@
 thm lam_bp.induct
 thm lam_bp.inducts
 thm lam_bp.distinct
+thm lam_bp.supp
 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
-thm lam_bp.fv[simplified lam_bp.supp]
+thm lam_bp.fv[simplified lam_bp.supp(1-2)]
 
 end