clarified signature;

--- a/src/Pure/Isar/class.ML	Mon May 15 20:37:53 2023 +0200
+++ b/src/Pure/Isar/class.ML	Mon May 15 20:55:17 2023 +0200
@@ -157,9 +157,8 @@
 val base_morphism = #base_morph oo the_class_data;
 
 fun morphism thy class =
-  (case Element.eq_morphism thy (these_defs thy [class]) of
-    SOME eq_morph => base_morphism thy class $> eq_morph
-  | NONE => base_morphism thy class);
+  base_morphism thy class $>
+  Morphism.default (Element.eq_morphism thy (these_defs thy [class]));
 
 val export_morphism = #export_morph oo the_class_data;
 

--- 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;

--- a/src/Pure/Isar/locale.ML	Mon May 15 20:37:53 2023 +0200
+++ b/src/Pure/Isar/locale.ML	Mon May 15 20:55:17 2023 +0200
@@ -538,7 +538,7 @@
   |> pair (Idents.get context)
   |> roundup (Context.theory_of context)
       (activate_notes_trace init_element Morphism.transfer_morphism'' context export)
-      (the_default Morphism.identity export) dep
+      (Morphism.default export) dep
   |-> Idents.put
   |> Context_Position.restore_visible_generic context;
 

--- a/src/Pure/morphism.ML	Mon May 15 20:37:53 2023 +0200
+++ b/src/Pure/morphism.ML	Mon May 15 20:55:17 2023 +0200
@@ -32,6 +32,7 @@
   val thm: morphism -> thm -> thm
   val cterm: morphism -> cterm -> cterm
   val identity: morphism
+  val default: morphism option -> morphism
   val compose: morphism -> morphism -> morphism
   val transform: morphism -> (morphism -> 'a) -> morphism -> 'a
   val form: (morphism -> 'a) -> 'a
@@ -106,6 +107,8 @@
 
 val identity = morphism "" {binding = [], typ = [], term = [], fact = []};
 
+val default = the_default identity;
+
 fun compose phi1 phi2 =
   if is_identity phi1 then phi2
   else if is_identity phi2 then phi1