--- a/Nominal/Nominal2.thy	Tue Dec 28 19:51:25 2010 +0000
+++ b/Nominal/Nominal2.thy	Thu Dec 30 10:00:09 2010 +0000
@@ -4,10 +4,9 @@
 uses ("nominal_dt_rawfuns.ML")
      ("nominal_dt_alpha.ML")
      ("nominal_dt_quot.ML")
-     ("induction_schema.ML")
+     ("nominal_induct.ML")
 begin
 
-use "induction_schema.ML"
 
 use "nominal_dt_rawfuns.ML"
 ML {* open Nominal_Dt_RawFuns *}
@@ -18,6 +17,12 @@
 use "nominal_dt_quot.ML"
 ML {* open Nominal_Dt_Quot *}
 
+(*****************************************)
+(* setup for induction principles method *)
+use "nominal_induct.ML"
+method_setup nominal_induct =
+  {* NominalInduct.nominal_induct_method *}
+  {* nominal induction *}
 
 ML {*
 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)