src/Pure/Isar/theory_target.ML
changeset 33537 06c87d2c5b5a
parent 33519 e31a85f92ce9
child 33553 35f2b30593a8
     1.1 --- a/src/Pure/Isar/theory_target.ML	Mon Nov 09 19:42:33 2009 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Nov 09 20:47:39 2009 +0100
     1.3 @@ -190,9 +190,7 @@
     1.4      val b' = Morphism.binding phi b;
     1.5      val rhs' = Morphism.term phi rhs;
     1.6      val arg = (b', Term.close_schematic_term rhs');
     1.7 -(*    val similar_body = Type.similar_types (rhs, rhs'); *)
     1.8 -    val same_shape = op aconv o pairself (Term.map_types (fn _ => Term.dummyT));
     1.9 -    val similar_body = same_shape (rhs, rhs');
    1.10 +    val same_shape = Term.aconv_untyped (rhs, rhs');
    1.11      (* FIXME workaround based on educated guess *)
    1.12      val prefix' = Binding.prefix_of b';
    1.13      val class_global =
    1.14 @@ -200,12 +198,12 @@
    1.15        not (null prefix') andalso
    1.16        fst (snd (split_last prefix')) = Class_Target.class_prefix target;
    1.17    in
    1.18 -    not (is_class andalso (similar_body orelse class_global)) ?
    1.19 +    not (is_class andalso (same_shape orelse class_global)) ?
    1.20        (Context.mapping_result
    1.21          (Sign.add_abbrev PrintMode.internal arg)
    1.22          (ProofContext.add_abbrev PrintMode.internal arg)
    1.23        #-> (fn (lhs' as Const (d, _), _) =>
    1.24 -          similar_body ?
    1.25 +          same_shape ?
    1.26              (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
    1.27               Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
    1.28    end;