1.1 --- a/src/Pure/Isar/theory_target.ML Fri Nov 14 08:50:10 2008 +0100
1.2 +++ b/src/Pure/Isar/theory_target.ML Fri Nov 14 08:50:11 2008 +0100
1.3 @@ -186,14 +186,14 @@
1.4 let
1.5 val c' = Morphism.name phi c;
1.6 val rhs' = Morphism.term phi rhs;
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.base name'
1.14 - andalso Class.class_prefix target = hd (NameSpace.explode name');
1.15 + val class_global = Name.name_of c = Name.name_of c'
1.16 + andalso not (null (Name.prefix_of c'))
1.17 + andalso (fst o snd o split_last) (Name.prefix_of c') = Class.class_prefix target;
1.18 in
1.19 not (is_class andalso (similar_body orelse class_global)) ?
1.20 (Context.mapping_result