--- a/Nominal/Test.thy	Tue Mar 16 12:08:37 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 16 15:27:47 2010 +0100
@@ -6,8 +6,9 @@
 
 atom_decl name
 
-ML {* val cheat_alpha_eqvt = ref false *}
-ML {* val cheat_fv_eqvt = ref false *}
+ML {* val _ = cheat_alpha_eqvt := false *}
+ML {* val _ = cheat_fv_eqvt := false *}
+ML {* val _ = recursive := false *}
 
 (*
 nominal_datatype lam =
@@ -60,7 +61,10 @@
 lemma alpha_bi:
   shows "alpha_bi pi b b' = True"
 apply(induct b rule: lam_bp_inducts(2))
-sorry
+apply(simp_all)
+apply(induct b' rule: lam_bp_inducts(2))
+apply (simp_all add: lam_bp_inject)
+done
 
 lemma fv_bi:
   shows "fv_bi b = {}"