--- 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)

--- a/Nominal/Nominal2_Base.thy	Thu Oct 04 11:10:23 2012 +0100
+++ b/Nominal/Nominal2_Base.thy	Thu Oct 04 12:44:43 2012 +0100
@@ -11,12 +11,6 @@
         "~~/src/HOL/Library/FinFun"
 keywords
   "atom_decl" "equivariance" :: thy_decl 
-uses ("nominal_basics.ML")
-     ("nominal_thmdecls.ML")
-     ("nominal_permeq.ML")
-     ("nominal_library.ML")
-     ("nominal_atoms.ML")
-     ("nominal_eqvt.ML")
 begin
 
 section {* Atoms and Sorts *}
@@ -768,14 +762,14 @@
 
 subsection {* Basic functions about permutations *}
 
-use "nominal_basics.ML"
+ML_file "nominal_basics.ML"
 
 
 subsection {* Eqvt infrastructure *}
 
 text {* Setup of the theorem attributes @{text eqvt} and @{text eqvt_raw} *}
 
-use "nominal_thmdecls.ML"
+ML_file "nominal_thmdecls.ML"
 setup "Nominal_ThmDecls.setup"
 
 
@@ -817,7 +811,7 @@
 
 text {* provides perm_simp methods *}
 
-use "nominal_permeq.ML"
+ML_file "nominal_permeq.ML"
 
 method_setup perm_simp =
  {* Nominal_Permeq.args_parser >> Nominal_Permeq.perm_simp_meth *}
@@ -3235,7 +3229,7 @@
 
 section {* Library functions for the nominal infrastructure *}
 
-use "nominal_library.ML"
+ML_file "nominal_library.ML"
 
 
 
@@ -3425,12 +3419,12 @@
 
 text {* at the moment only single-sort concrete atoms are supported *}
 
-use "nominal_atoms.ML"
+ML_file "nominal_atoms.ML"
 
 
 section {* automatic equivariance procedure for inductive definitions *}
 
-use "nominal_eqvt.ML"
+ML_file "nominal_eqvt.ML"