1.1 --- a/src/Pure/Isar/proof_context.ML	Mon Nov 09 19:42:33 2009 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Mon Nov 09 20:47:39 2009 +0100
     1.3 @@ -1032,7 +1032,10 @@
     1.4      (Local_Syntax.update_modesyntax (theory_of ctxt) add mode (map_filter (const_syntax ctxt) args));
     1.5  
     1.6  fun target_notation add mode args phi =
     1.7 -  let val args' = filter (fn (t, _) => Type.similar_types (t, Morphism.term phi t)) args;
     1.8 +  let
     1.9 +    val args' = args |> map_filter (fn (t, mx) =>
    1.10 +      let val t' = Morphism.term phi t
    1.11 +      in if Term.aconv_untyped (t, t') then SOME (t', mx) else NONE end);
    1.12    in Context.mapping (Sign.notation add mode args') (notation add mode args') end;
    1.13  
    1.14  end;

     2.1 --- a/src/Pure/Isar/theory_target.ML	Mon Nov 09 19:42:33 2009 +0100
     2.2 +++ b/src/Pure/Isar/theory_target.ML	Mon Nov 09 20:47:39 2009 +0100
     2.3 @@ -190,9 +190,7 @@
     2.4      val b' = Morphism.binding phi b;
     2.5      val rhs' = Morphism.term phi rhs;
     2.6      val arg = (b', Term.close_schematic_term rhs');
     2.7 -(*    val similar_body = Type.similar_types (rhs, rhs'); *)
     2.8 -    val same_shape = op aconv o pairself (Term.map_types (fn _ => Term.dummyT));
     2.9 -    val similar_body = same_shape (rhs, rhs');
    2.10 +    val same_shape = Term.aconv_untyped (rhs, rhs');
    2.11      (* FIXME workaround based on educated guess *)
    2.12      val prefix' = Binding.prefix_of b';
    2.13      val class_global =
    2.14 @@ -200,12 +198,12 @@
    2.15        not (null prefix') andalso
    2.16        fst (snd (split_last prefix')) = Class_Target.class_prefix target;
    2.17    in
    2.18 -    not (is_class andalso (similar_body orelse class_global)) ?
    2.19 +    not (is_class andalso (same_shape orelse class_global)) ?
    2.20        (Context.mapping_result
    2.21          (Sign.add_abbrev PrintMode.internal arg)
    2.22          (ProofContext.add_abbrev PrintMode.internal arg)
    2.23        #-> (fn (lhs' as Const (d, _), _) =>
    2.24 -          similar_body ?
    2.25 +          same_shape ?
    2.26              (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
    2.27               Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
    2.28    end;

     3.1 --- a/src/Pure/term.ML	Mon Nov 09 19:42:33 2009 +0100
     3.2 +++ b/src/Pure/term.ML	Mon Nov 09 20:47:39 2009 +0100
     3.3 @@ -146,6 +146,7 @@
     3.4    val eq_ix: indexname * indexname -> bool
     3.5    val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
     3.6    val eq_var: (indexname * typ) * (indexname * typ) -> bool
     3.7 +  val aconv_untyped: term * term -> bool
     3.8    val could_unify: term * term -> bool
     3.9    val strip_abs_eta: int -> term -> (string * typ) list * term
    3.10    val match_bvars: (term * term) * (string * string) list -> (string * string) list
    3.11 @@ -524,6 +525,17 @@
    3.12      | (Abs (_, T1, t1), Abs (_, T2, t2)) => t1 aconv t2 andalso T1 = T2
    3.13      | (a1, a2) => a1 = a2);
    3.14  
    3.15 +fun aconv_untyped (tm1, tm2) =
    3.16 +  pointer_eq (tm1, tm2) orelse
    3.17 +    (case (tm1, tm2) of
    3.18 +      (t1 $ u1, t2 $ u2) => aconv_untyped (t1, t2) andalso aconv_untyped (u1, u2)
    3.19 +    | (Abs (_, _, t1), Abs (_, _, t2)) => aconv_untyped (t1, t2)
    3.20 +    | (Const (a, _), Const (b, _)) => a = b
    3.21 +    | (Free (x, _), Free (y, _)) => x = y
    3.22 +    | (Var (xi, _), Var (yj, _)) => xi = yj
    3.23 +    | (Bound i, Bound j) => i = j
    3.24 +    | _ => false);
    3.25 +
    3.26  
    3.27  (*A fast unification filter: true unless the two terms cannot be unified.
    3.28    Terms must be NORMAL.  Treats all Vars as distinct. *)

     4.1 --- a/src/Pure/type.ML	Mon Nov 09 19:42:33 2009 +0100
     4.2 +++ b/src/Pure/type.ML	Mon Nov 09 20:47:39 2009 +0100
     4.3 @@ -42,7 +42,6 @@
     4.4  
     4.5    (*special treatment of type vars*)
     4.6    val strip_sorts: typ -> typ
     4.7 -  val similar_types: term * term -> bool
     4.8    val no_tvars: typ -> typ
     4.9    val varify: (string * sort) list -> term -> ((string * sort) * indexname) list * term
    4.10    val freeze_thaw_type: typ -> typ * (typ -> typ)
    4.11 @@ -236,23 +235,6 @@
    4.12    | strip_sorts (TVar (xi, _)) = TVar (xi, []);
    4.13  
    4.14  
    4.15 -(* equivalence up to renaming of atomic types *)
    4.16 -
    4.17 -local
    4.18 -
    4.19 -fun standard_types t =
    4.20 -  let
    4.21 -    val Ts = fold_types (fold_atyps (insert (op =))) t [];
    4.22 -    val Ts' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length Ts));
    4.23 -  in map_types (map_atyps (perhaps (AList.lookup (op =) (Ts ~~ Ts')))) t end;
    4.24 -
    4.25 -in
    4.26 -
    4.27 -val similar_types = op aconv o pairself (Term.map_types strip_sorts o standard_types);
    4.28 -
    4.29 -end;
    4.30 -
    4.31 -
    4.32  (* no_tvars *)
    4.33  
    4.34  fun no_tvars T =