diff -r 16ffbc8442ca -r ffb5a181844b Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Sun Dec 26 16:35:16 2010 +0000
+++ b/Nominal/Nominal2.thy	Tue Dec 28 00:20:50 2010 +0000
@@ -4,8 +4,10 @@
 uses ("nominal_dt_rawfuns.ML")
      ("nominal_dt_alpha.ML")
      ("nominal_dt_quot.ML")
+     ("induction_schema.ML")
 begin
 
+use "induction_schema.ML"
 
 use "nominal_dt_rawfuns.ML"
 ML {* open Nominal_Dt_RawFuns *}
@@ -533,7 +535,7 @@
   val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts bclauses qbn_finite_thms qeq_iffs'
     qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms
 
-  val qstrong_induct_thm = prove_strong_induct lthyC qinduct qexhausts bclauses
+  val qstrong_induct_thm = prove_strong_induct lthyC qinduct qstrong_exhaust_thms bclauses
 
 
   (* noting the theorems *)