diff -r 995d47b09ab4 -r 3e6f4320669f Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Thu Oct 04 11:10:23 2012 +0100
+++ b/Nominal/Nominal2.thy	Thu Oct 04 12:44:43 2012 +0100
@@ -5,51 +5,40 @@
   "nominal_datatype" :: thy_decl and
   "nominal_primrec" "nominal_inductive" :: thy_goal and
   "avoids" "binds"
-uses ("nominal_dt_rawfuns.ML")
-     ("nominal_dt_alpha.ML")
-     ("nominal_dt_quot.ML")
-     ("nominal_induct.ML")
-     ("nominal_inductive.ML")
-     ("nominal_function_common.ML")
-     ("nominal_function_core.ML")
-     ("nominal_mutual.ML")
-     ("nominal_function.ML")
-     ("nominal_termination.ML")
-     ("nominal_dt_data.ML")
 begin
 
-use "nominal_dt_data.ML"
+ML_file "nominal_dt_data.ML"
 ML {* open Nominal_Dt_Data *}
 
-use "nominal_dt_rawfuns.ML"
+ML_file "nominal_dt_rawfuns.ML"
 ML {* open Nominal_Dt_RawFuns *}
 
-use "nominal_dt_alpha.ML"
+ML_file "nominal_dt_alpha.ML"
 ML {* open Nominal_Dt_Alpha *}
 
-use "nominal_dt_quot.ML"
+ML_file "nominal_dt_quot.ML"
 ML {* open Nominal_Dt_Quot *}
 
 (*****************************************)
 (* setup for induction principles method *)
-use "nominal_induct.ML"
+ML_file "nominal_induct.ML"
 method_setup nominal_induct =
   {* NominalInduct.nominal_induct_method *}
   {* nominal induction *}
 
 (****************************************************)
 (* inductive definition involving nominal datatypes *)
-use "nominal_inductive.ML" 
+ML_file "nominal_inductive.ML" 
 
 
 (***************************************)
 (* forked code of the function package *)
 (* for defining nominal functions      *)
-use "nominal_function_common.ML"
-use "nominal_function_core.ML"
-use "nominal_mutual.ML"
-use "nominal_function.ML"
-use "nominal_termination.ML"
+ML_file "nominal_function_common.ML"
+ML_file "nominal_function_core.ML"
+ML_file "nominal_mutual.ML"
+ML_file "nominal_function.ML"
+ML_file "nominal_termination.ML"
 
 ML {*
 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)