src/Pure/Isar/theory_target.ML
changeset 25372 a718f1ccaf1a
parent 25320 618247e82f3d
child 25381 c100bf5bd6b8
     1.1 --- a/src/Pure/Isar/theory_target.ML	Sat Nov 10 14:31:21 2007 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Sat Nov 10 14:31:22 2007 +0100
     1.3 @@ -177,15 +177,16 @@
     1.4      val rhs' = Morphism.term phi rhs;
     1.5      val legacy_arg = (c', Term.close_schematic_term (Logic.legacy_varify rhs'));
     1.6      val arg = (c', Term.close_schematic_term rhs');
     1.7 +    val similar_body = Type.similar_types (rhs, rhs');
     1.8      (* FIXME workaround based on educated guess *)
     1.9 -    val class_global = is_class andalso c' = NameSpace.qualified (Class.class_prefix target) c;
    1.10 +    val class_global = c' = NameSpace.qualified (Class.class_prefix target) c;
    1.11    in
    1.12 -    not class_global ?
    1.13 +    not (is_class andalso (similar_body orelse class_global)) ?
    1.14        (Context.mapping_result
    1.15          (Sign.add_abbrev PrintMode.internal pos legacy_arg)
    1.16          (ProofContext.add_abbrev PrintMode.internal pos arg)
    1.17        #-> (fn (lhs' as Const (d, _), _) =>
    1.18 -          Type.similar_types (rhs, rhs') ?
    1.19 +          similar_body ?
    1.20              (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
    1.21               Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
    1.22    end;