# HG changeset patch
# User wenzelm
# Date 1737485353 -3600
# Node ID 5be5b2114ecd0e0d63cbb4f5347bef8344e3aa09
# Parent  ee680c69de38a2074220ffa394c312950a544bcb
tuned;

diff -r ee680c69de38 -r 5be5b2114ecd src/HOL/Import/import_rule.ML
--- a/src/HOL/Import/import_rule.ML	Tue Jan 21 19:26:39 2025 +0100
+++ b/src/HOL/Import/import_rule.ML	Tue Jan 21 19:49:13 2025 +0100
@@ -275,10 +275,9 @@
       Abs_name = Binding.name abs_name,
       type_definition_name = Binding.name ("type_definition_" ^ tycname)}
     val ((_, typedef_info), thy') =
-     Named_Target.theory_map_result (apsnd o Typedef.transform_info)
-     (Typedef.add_typedef {overloaded = false}
+     Typedef.add_typedef_global {overloaded = false}
        (Binding.name tycname, map (rpair dummyS) tnames, NoSyn) c
-       (SOME typedef_bindings) (fn ctxt => resolve_tac ctxt [th2] 1)) thy
+       (SOME typedef_bindings) (fn ctxt => resolve_tac ctxt [th2] 1) thy
     val aty = Thm.global_ctyp_of thy' (#abs_type (#1 typedef_info))
     val th = freezeT thy' (#type_definition (#2 typedef_info))
     val (rep, abs) = Thm.dest_binop (Thm.dest_fun (HOLogic.dest_judgment (Thm.cprop_of th)))
diff -r ee680c69de38 -r 5be5b2114ecd src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Tue Jan 21 19:26:39 2025 +0100
+++ b/src/HOL/Tools/typedef.ML	Tue Jan 21 19:49:13 2025 +0100
@@ -302,7 +302,7 @@
 
 fun add_typedef_global overloaded typ set opt_bindings tac =
   Named_Target.theory_map_result (apsnd o transform_info)
-    (add_typedef overloaded typ set opt_bindings tac)
+    (add_typedef overloaded typ set opt_bindings tac);
 
 
 (* typedef: proof interface *)