--- a/Nominal/Ex/Ex1rec.thy	Thu Jun 03 15:02:52 2010 +0200
+++ b/Nominal/Ex/Ex1rec.thy	Mon Jun 07 11:43:01 2010 +0200
@@ -2,10 +2,9 @@
 imports "../NewParser"
 begin
 
-atom_decl name
+declare [[STEPS = 9]]
 
-ML {* val _ = cheat_supp_eq := true *}
-ML {* val _ = cheat_equivp := true *}
+atom_decl name
 
 nominal_datatype lam =
   Var "name"
@@ -19,6 +18,9 @@
 where
   "bi (Bp x t) = {atom x}"
 
+
+thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros
+
 thm lam_bp.fv
 thm lam_bp.eq_iff[no_vars]
 thm lam_bp.bn