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