# HG changeset patch
# User wenzelm
# Date 1257796059 -3600
# Node ID 06c87d2c5b5a975ea76c90de97cffb55e4fab352
# Parent  fd28b7399f2ba3b172b3d30d24b205e1d1b07d88
locale_const/target_notation: uniform use of Term.aconv_untyped;
target_notation: pass on transformed term formally;
removed obsolete Type.similar_types;

diff -r fd28b7399f2b -r 06c87d2c5b5a src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Nov 09 19:42:33 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Mon Nov 09 20:47:39 2009 +0100
@@ -1032,7 +1032,10 @@
     (Local_Syntax.update_modesyntax (theory_of ctxt) add mode (map_filter (const_syntax ctxt) args));
 
 fun target_notation add mode args phi =
-  let val args' = filter (fn (t, _) => Type.similar_types (t, Morphism.term phi t)) args;
+  let
+    val args' = args |> map_filter (fn (t, mx) =>
+      let val t' = Morphism.term phi t
+      in if Term.aconv_untyped (t, t') then SOME (t', mx) else NONE end);
   in Context.mapping (Sign.notation add mode args') (notation add mode args') end;
 
 end;
diff -r fd28b7399f2b -r 06c87d2c5b5a src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Mon Nov 09 19:42:33 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Mon Nov 09 20:47:39 2009 +0100
@@ -190,9 +190,7 @@
     val b' = Morphism.binding phi b;
     val rhs' = Morphism.term phi rhs;
     val arg = (b', Term.close_schematic_term rhs');
-(*    val similar_body = Type.similar_types (rhs, rhs'); *)
-    val same_shape = op aconv o pairself (Term.map_types (fn _ => Term.dummyT));
-    val similar_body = same_shape (rhs, rhs');
+    val same_shape = Term.aconv_untyped (rhs, rhs');
     (* FIXME workaround based on educated guess *)
     val prefix' = Binding.prefix_of b';
     val class_global =
@@ -200,12 +198,12 @@
       not (null prefix') andalso
       fst (snd (split_last prefix')) = Class_Target.class_prefix target;
   in
-    not (is_class andalso (similar_body orelse class_global)) ?
+    not (is_class andalso (same_shape orelse class_global)) ?
       (Context.mapping_result
         (Sign.add_abbrev PrintMode.internal arg)
         (ProofContext.add_abbrev PrintMode.internal arg)
       #-> (fn (lhs' as Const (d, _), _) =>
-          similar_body ?
+          same_shape ?
             (Context.mapping (Sign.revert_abbrev mode d) (ProofContext.revert_abbrev mode d) #>
              Morphism.form (ProofContext.target_notation true prmode [(lhs', mx)]))))
   end;
diff -r fd28b7399f2b -r 06c87d2c5b5a src/Pure/term.ML
--- a/src/Pure/term.ML	Mon Nov 09 19:42:33 2009 +0100
+++ b/src/Pure/term.ML	Mon Nov 09 20:47:39 2009 +0100
@@ -146,6 +146,7 @@
   val eq_ix: indexname * indexname -> bool
   val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
   val eq_var: (indexname * typ) * (indexname * typ) -> bool
+  val aconv_untyped: term * term -> bool
   val could_unify: term * term -> bool
   val strip_abs_eta: int -> term -> (string * typ) list * term
   val match_bvars: (term * term) * (string * string) list -> (string * string) list
@@ -524,6 +525,17 @@
     | (Abs (_, T1, t1), Abs (_, T2, t2)) => t1 aconv t2 andalso T1 = T2
     | (a1, a2) => a1 = a2);
 
+fun aconv_untyped (tm1, tm2) =
+  pointer_eq (tm1, tm2) orelse
+    (case (tm1, tm2) of
+      (t1 $ u1, t2 $ u2) => aconv_untyped (t1, t2) andalso aconv_untyped (u1, u2)
+    | (Abs (_, _, t1), Abs (_, _, t2)) => aconv_untyped (t1, t2)
+    | (Const (a, _), Const (b, _)) => a = b
+    | (Free (x, _), Free (y, _)) => x = y
+    | (Var (xi, _), Var (yj, _)) => xi = yj
+    | (Bound i, Bound j) => i = j
+    | _ => false);
+
 
 (*A fast unification filter: true unless the two terms cannot be unified.
   Terms must be NORMAL.  Treats all Vars as distinct. *)
diff -r fd28b7399f2b -r 06c87d2c5b5a src/Pure/type.ML
--- a/src/Pure/type.ML	Mon Nov 09 19:42:33 2009 +0100
+++ b/src/Pure/type.ML	Mon Nov 09 20:47:39 2009 +0100
@@ -42,7 +42,6 @@
 
   (*special treatment of type vars*)
   val strip_sorts: typ -> typ
-  val similar_types: term * term -> bool
   val no_tvars: typ -> typ
   val varify: (string * sort) list -> term -> ((string * sort) * indexname) list * term
   val freeze_thaw_type: typ -> typ * (typ -> typ)
@@ -236,23 +235,6 @@
   | strip_sorts (TVar (xi, _)) = TVar (xi, []);
 
 
-(* equivalence up to renaming of atomic types *)
-
-local
-
-fun standard_types t =
-  let
-    val Ts = fold_types (fold_atyps (insert (op =))) t [];
-    val Ts' = map (fn a => TFree (a, [])) (Name.invents Name.context Name.aT (length Ts));
-  in map_types (map_atyps (perhaps (AList.lookup (op =) (Ts ~~ Ts')))) t end;
-
-in
-
-val similar_types = op aconv o pairself (Term.map_types strip_sorts o standard_types);
-
-end;
-
-
 (* no_tvars *)
 
 fun no_tvars T =