--- a/Nominal/Test.thy	Mon Mar 15 17:52:31 2010 +0100
+++ b/Nominal/Test.thy	Mon Mar 15 23:42:56 2010 +0100
@@ -6,6 +6,9 @@
 
 atom_decl name
 
+ML {* val cheat_alpha_eqvt = ref false *}
+ML {* val cheat_fv_eqvt = ref false *}
+
 (*
 nominal_datatype lam =
   VAR "name"
@@ -37,11 +40,11 @@
 thm lam_bp_bn
 thm lam_bp_perm
 thm lam_bp_induct
+thm lam_bp_inducts
 thm lam_bp_distinct
 ML {* Sign.of_sort @{theory} (@{typ lam}, @{sort fs}) *}
 
 term "supp (x :: lam)"
-lemmas lam_bp_inducts = lam_raw_bp_raw.inducts[quot_lifted]
 
 (* maybe should be added to Infinite.thy *)
 lemma infinite_Un:
@@ -50,13 +53,7 @@
 
 lemma bi_eqvt:
   shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)"
-apply(induct b rule: lam_bp_inducts(2))
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp add: lam_bp_bn lam_bp_perm)
-apply(simp add: eqvts)
-done
+  by (rule eqvts)
 
 term alpha_bi
 
@@ -366,6 +363,7 @@
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_bn
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_perm
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_induct
+thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_inducts
 thm mexp_body_defn_sexp_sbody_spec_tyty_path_trmtrm_distinct
 
 (* example 3 from Peter Sewell's bestiary *)