similar_types: uniform treatment of TFrees/TVars;

--- a/src/Pure/type.ML	Sat Nov 10 23:03:56 2007 +0100
+++ b/src/Pure/type.ML	Sat Nov 10 23:03:57 2007 +0100
@@ -243,21 +243,15 @@
   | strip_sorts (TVar (xi, _)) = TVar (xi, []);
 
 
-(* equivalence up to renaming of types variables *)
+(* equivalence up to renaming of atomic types *)
 
 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;
+    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