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