--- a/src/Pure/Isar/expression.ML Mon May 15 20:37:53 2023 +0200
+++ b/src/Pure/Isar/expression.ML Mon May 15 20:55:17 2023 +0200
@@ -407,7 +407,7 @@
|> map (abs_def ctxt')
|> Variable.export_terms ctxt' ctxt
|> Element.eq_term_morphism (Proof_Context.theory_of ctxt)
- |> the_default Morphism.identity;
+ |> Morphism.default;
val ctxt'' = Locale.activate_declarations (loc, inst_morph $> rewrite_morph) ctxt;
val eqnss' = eqnss @ [attrss ~~ Variable.export_terms ctxt' ctxt eqns'];
in (i + 1, insts', eqnss', ctxt'') end;