src/Pure/Isar/class.ML

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