--- 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