--- a/src/HOL/Import/Import_Setup.thy Sat Jan 18 10:59:00 2025 +0100
+++ b/src/HOL/Import/Import_Setup.thy Sat Jan 18 11:03:18 2025 +0100
@@ -11,6 +11,17 @@
begin
ML_file \<open>import_data.ML\<close>
+
+text \<open>
+ Initial type and constant maps, for types and constants that are not
+ defined, which means their definitions do not appear in the proof dump.
+\<close>
+import_type_map bool : bool
+import_type_map "fun" : "fun"
+import_type_map ind : ind
+import_const_map "=" : HOL.eq
+import_const_map "@" : Eps
+
ML_file \<open>import_rule.ML\<close>
end
--- a/src/HOL/Import/import_data.ML Sat Jan 18 10:59:00 2025 +0100
+++ b/src/HOL/Import/import_data.ML Sat Jan 18 11:03:18 2025 +0100
@@ -120,14 +120,4 @@
((Parse.name --| \<^keyword>\<open>:\<close>) -- Parse.const >>
(fn (c, d) => Toplevel.theory (add_const_map_cmd c d)))
-(*Initial type and constant maps, for types and constants that are not
- defined, which means their definitions do not appear in the proof dump.*)
-val _ =
- Theory.setup
- (add_typ_map "bool" \<^type_name>\<open>bool\<close> #>
- add_typ_map "fun" \<^type_name>\<open>fun\<close> #>
- add_typ_map "ind" \<^type_name>\<open>ind\<close> #>
- add_const_map "=" \<^const_name>\<open>HOL.eq\<close> #>
- add_const_map "@" \<^const_name>\<open>Eps\<close>)
-
end