src/HOL/Nominal/Nominal.thy

 theory Nominal 
 imports Main Infinite_Set
 uses
   ("nominal_thmdecls.ML")
   ("nominal_atoms.ML")
-  ("nominal.ML")
+  ("nominal_datatype.ML")
   ("nominal_induct.ML") 
   ("nominal_permeq.ML")
   ("nominal_fresh_fun.ML")
   ("nominal_primrec.ML")
   ("nominal_inductive.ML")

 (************************************************)
 (* main file for constructing nominal datatypes *)
 lemma allE_Nil: assumes "\<forall>x. P x" obtains "P []"
   using assms ..
 
-use "nominal.ML"
+use "nominal_datatype.ML"
 
 (******************************************************)
 (* primitive recursive functions on nominal datatypes *)
 use "nominal_primrec.ML"