src/Pure/Isar/class_declaration.ML
changeset 54740 91f54d386680
parent 52788 da1fdbfebd39
child 54742 7a86358a3c0b
     1.1 --- a/src/Pure/Isar/class_declaration.ML	Fri Dec 13 14:58:47 2013 +0100
     1.2 +++ b/src/Pure/Isar/class_declaration.ML	Fri Dec 13 20:20:15 2013 +0100
     1.3 @@ -64,7 +64,7 @@
     1.4  
     1.5      (* canonical interpretation *)
     1.6      val base_morph = inst_morph
     1.7 -      $> Morphism.binding_morphism (Binding.prefix false (Class.class_prefix class))
     1.8 +      $> Morphism.binding_morphism "class_binding" (Binding.prefix false (Class.class_prefix class))
     1.9        $> Element.satisfy_morphism (the_list some_witn);
    1.10      val eq_morph = Element.eq_morphism thy (Class.these_defs thy sups);
    1.11