diff -r d72ca5742f80 -r c0eafbd55de3 src/HOL/Import/Import_Setup.thy
--- a/src/HOL/Import/Import_Setup.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Import/Import_Setup.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -7,12 +7,11 @@
 
 theory Import_Setup
 imports "~~/src/HOL/Parity" "~~/src/HOL/Fact"
-keywords
-    "import_type_map" :: thy_decl and "import_const_map" :: thy_decl and
-    "import_file" :: thy_decl
-uses "import_data.ML" ("import_rule.ML")
+keywords "import_type_map" "import_const_map" "import_file" :: thy_decl
 begin
 
+ML_file "import_data.ML"
+
 lemma light_ex_imp_nonempty:
   "P t \<Longrightarrow> \<exists>x. x \<in> Collect P"
   by auto
@@ -27,7 +26,7 @@
   "(\<And>x. f x = g x) \<Longrightarrow> f = g"
   by auto
 
-use "import_rule.ML"
+ML_file "import_rule.ML"
 
 end