src/HOL/Nominal/Nominal.thy

   ("nominal_induct.ML") 
   ("nominal_permeq.ML")
   ("nominal_fresh_fun.ML")
   ("nominal_primrec.ML")
   ("nominal_inductive.ML")
+  ("nominal_inductive2.ML")
 begin 
 
 section {* Permutations *}
 (*======================*)
 

 use "nominal_primrec.ML"
 
 (****************************************************)
 (* inductive definition involving nominal datatypes *)
 use "nominal_inductive.ML"
+use "nominal_inductive2.ML"
 
 (*****************************************)
 (* setup for induction principles method *)
 use "nominal_induct.ML";
 method_setup nominal_induct =