--- a/src/Pure/Isar/class_declaration.ML Fri Dec 13 14:58:47 2013 +0100
+++ b/src/Pure/Isar/class_declaration.ML Fri Dec 13 20:20:15 2013 +0100
@@ -64,7 +64,7 @@
(* canonical interpretation *)
val base_morph = inst_morph
- $> Morphism.binding_morphism (Binding.prefix false (Class.class_prefix class))
+ $> Morphism.binding_morphism "class_binding" (Binding.prefix false (Class.class_prefix class))
$> Element.satisfy_morphism (the_list some_witn);
val eq_morph = Element.eq_morphism thy (Class.these_defs thy sups);