# HG changeset patch
# User wenzelm
# Date 1737194598 -3600
# Node ID aa28d82d6b66264ab7fa7f010bb0cc5092d69e5b
# Parent  95388e387ba20a3e89df8fdc37a5da33ed6ae107
tuned;

diff -r 95388e387ba2 -r aa28d82d6b66 src/HOL/Import/Import_Setup.thy
--- 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
diff -r 95388e387ba2 -r aa28d82d6b66 src/HOL/Import/import_data.ML
--- 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