diff -r d555983054f3 -r b6c886b7184f src/Pure/Isar/expression.ML
--- 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;