replaced Term.equiv_types by Type.similar_types;

--- a/src/Pure/Isar/proof_context.ML	Thu Oct 11 19:10:23 2007 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Oct 11 19:10:24 2007 +0200
@@ -1013,7 +1013,7 @@
     (LocalSyntax.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, _) => Term.equiv_types (t, Morphism.term phi t)) args;
+  let val args' = filter (fn (t, _) => Type.similar_types (t, Morphism.term phi t)) args;
   in Context.mapping (Sign.notation add mode args') (notation add mode args') end;
 
 end;

--- a/src/Pure/term.ML	Thu Oct 11 19:10:23 2007 +0200
+++ b/src/Pure/term.ML	Thu Oct 11 19:10:24 2007 +0200
@@ -162,7 +162,6 @@
   val add_tfrees: term -> (string * sort) list -> (string * sort) list
   val add_frees: term -> (string * typ) list -> (string * typ) list
   val hidden_polymorphism: term -> typ -> (indexname * sort) list
-  val equiv_types: term * term -> bool
   val strip_abs_eta: int -> term -> (string * typ) list * term
   val fast_indexname_ord: indexname * indexname -> order
   val indexname_ord: indexname * indexname -> order
@@ -535,29 +534,6 @@
     | (a1, a2) => a1 = a2);
 
 
-(* equivalence up to renaming of types variables *)
-
-local
-
-val invent_names = Name.invents Name.context Name.aT;
-
-fun standard_types t =
-  let
-    val tfrees = add_tfrees t [];
-    val tvars = add_tvars t [];
-    val env1 = map2 (fn (a, S) => fn a' => (TFree (a, S), TFree (a', [])))
-      tfrees (invent_names (length tfrees));
-    val env2 = map2 (fn ((a, i), S) => fn a' => (TVar ((a, i), S), TVar ((a', 0), [])))
-      tvars (invent_names (length tvars));
-  in map_types (map_atyps (perhaps (AList.lookup (op =) (env1 @ env2)))) t end;
-
-in
-
-val equiv_types = op aconv o pairself standard_types;
-
-end;
-
-
 (* fast syntactic ordering -- tuned for inequalities *)
 
 fun fast_indexname_ord ((x, i), (y, j)) =

--- a/src/Pure/type.ML	Thu Oct 11 19:10:23 2007 +0200
+++ b/src/Pure/type.ML	Thu Oct 11 19:10:24 2007 +0200
@@ -45,6 +45,7 @@
 
   (*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)
@@ -242,6 +243,29 @@
   | strip_sorts (TVar (xi, _)) = TVar (xi, []);
 
 
+(* equivalence up to renaming of types variables *)
+
+local
+
+val invent_names = Name.invents Name.context Name.aT;
+
+fun standard_types t =
+  let
+    val tfrees = Term.add_tfrees t [];
+    val tvars = Term.add_tvars t [];
+    val env1 = map2 (fn (a, S) => fn a' => (TFree (a, S), TFree (a', [])))
+      tfrees (invent_names (length tfrees));
+    val env2 = map2 (fn ((a, i), S) => fn a' => (TVar ((a, i), S), TVar ((a', 0), [])))
+      tvars (invent_names (length tvars));
+  in map_types (map_atyps (perhaps (AList.lookup (op =) (env1 @ env2)))) 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 =