tuned;

--- a/src/HOL/Import/import_data.ML	Sat Jan 18 11:03:18 2025 +0100
+++ b/src/HOL/Import/import_data.ML	Sat Jan 18 11:09:00 2025 +0100
@@ -97,15 +97,15 @@
   Theory.setup (Attrib.setup \<^binding>\<open>import_const\<close>
     (Scan.lift Parse.name --
       Scan.option (Scan.lift \<^keyword>\<open>:\<close> |-- Args.const {proper = true, strict = false}) >>
-      (fn (s1, s2) => Thm.declaration_attribute
-        (fn th => Context.mapping (add_const_def s1 th s2) I)))
+      (fn (c, d) => Thm.declaration_attribute
+        (fn th => Context.mapping (add_const_def c th d) I)))
     "declare a theorem as an equality that maps the given constant")
 
 val _ =
   Theory.setup (Attrib.setup \<^binding>\<open>import_type\<close>
     (Scan.lift (Parse.name -- Parse.name -- Parse.name) >>
-      (fn ((tyname, absname), repname) => Thm.declaration_attribute
-        (fn th => Context.mapping (add_typ_def tyname absname repname th) I)))
+      (fn ((c, abs), rep) => Thm.declaration_attribute
+        (fn th => Context.mapping (add_typ_def c abs rep th) I)))
     "declare a type_definition theorem as a map for an imported type with abs and rep")
 
 val _ =

--- a/src/HOL/Import/import_rule.ML	Sat Jan 18 11:03:18 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Sat Jan 18 11:09:00 2025 +0100
@@ -210,8 +210,9 @@
 fun tydef' tycname abs_name rep_name cP ct td_th thy =
   let
     val ctT = Thm.ctyp_of_cterm ct
-    val nonempty = Thm.instantiate' [SOME ctT] [SOME cP, SOME ct]
-      @{lemma "P t \<Longrightarrow> \<exists>x. x \<in> Collect P" by auto}
+    val nonempty =
+      Thm.instantiate' [SOME ctT] [SOME cP, SOME ct]
+        @{lemma "P t \<Longrightarrow> \<exists>x. x \<in> Collect P" by auto}
     val th2 = meta_mp nonempty td_th
     val c =
       (case Thm.concl_of th2 of