# HG changeset patch
# User wenzelm
# Date 1165952964 -3600
# Node ID 25b97f5057f270e72a7a134af6c27c76e90f15d2
# Parent  481094a3dd1f2e77a27bd0792a1687d709d3bf99
added equiv_types;

diff -r 481094a3dd1f -r 25b97f5057f2 src/Pure/term.ML
--- a/src/Pure/term.ML	Tue Dec 12 20:49:23 2006 +0100
+++ b/src/Pure/term.ML	Tue Dec 12 20:49:24 2006 +0100
@@ -161,6 +161,7 @@
   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
@@ -508,6 +509,29 @@
     | (a1, a2) => a1 = a2);
 
 
+(* equivalence up to renaming of types variables *)
+
+local
+
+val invent_names = Name.invents Name.context "'a";
+
+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)) =