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