--- a/src/HOL/Tools/typedef.ML Thu Feb 21 09:15:06 2019 +0000
+++ b/src/HOL/Tools/typedef.ML Thu Feb 21 09:15:07 2019 +0000
@@ -307,9 +307,8 @@
in typedef_result inhabited lthy' end;
fun add_typedef_global overloaded typ set opt_bindings tac =
- Named_Target.theory_init
- #> add_typedef overloaded typ set opt_bindings tac
- #> Local_Theory.exit_result_global (apsnd o transform_info);
+ Named_Target.theory_map_result (apsnd o transform_info)
+ (add_typedef overloaded typ set opt_bindings tac)
(* typedef: proof interface *)