--- a/src/Pure/Isar/local_theory.ML Sat May 20 14:48:06 2023 +0200
+++ b/src/Pure/Isar/local_theory.ML Sat May 20 16:12:37 2023 +0200
@@ -195,7 +195,8 @@
fun standard_morphism lthy ctxt =
Morphism.set_context' lthy
- (Proof_Context.norm_export_morphism lthy ctxt $>
+ (Proof_Context.export_morphism lthy ctxt $>
+ Morphism.thm_morphism' "Local_Theory.standard" (Goal.norm_result o Proof_Context.init_global) $>
Morphism.binding_morphism "Local_Theory.standard_binding"
(Name_Space.transform_binding (Proof_Context.naming_of lthy)));