--- a/Nominal/Test.thy	Mon Mar 15 13:56:17 2010 +0100
+++ b/Nominal/Test.thy	Mon Mar 15 14:32:05 2010 +0100
@@ -24,11 +24,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:
@@ -306,6 +306,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 *)