1.1 --- a/src/Pure/Isar/theory_target.ML	Mon Sep 22 08:00:27 2008 +0200
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Sep 22 08:00:28 2008 +0200
     1.3 @@ -189,12 +189,13 @@
     1.4      val c' = Morphism.name phi c;
     1.5      val rhs' = Morphism.term phi rhs;
     1.6      val name = Name.name_of c;
     1.7 -    val name' = Name.name_of c'
     1.8 +    val name' = Name.name_of c';
     1.9      val legacy_arg = (name', Term.close_schematic_term (Logic.legacy_varify rhs'));
    1.10      val arg = (name', Term.close_schematic_term rhs');
    1.11      val similar_body = Type.similar_types (rhs, rhs');
    1.12      (* FIXME workaround based on educated guess *)
    1.13 -    val class_global = name' = NameSpace.qualified (Class.class_prefix target) name;
    1.14 +    val class_global = name = NameSpace.base name'
    1.15 +      andalso Class.class_prefix target = hd (NameSpace.explode name');
    1.16    in
    1.17      not (is_class andalso (similar_body orelse class_global)) ?
    1.18        (Context.mapping_result