# HG changeset patch
# User wenzelm
# Date 1230670087 -3600
# Node ID 010b4dd637fe64c67b146e218dabc2f3dd8f3a72
# Parent  4621affa5c795951a085b4888a906ae8e3a207b2
varify: regular name context;

diff -r 4621affa5c79 -r 010b4dd637fe src/Pure/type.ML
--- a/src/Pure/type.ML	Tue Dec 30 21:47:11 2008 +0100
+++ b/src/Pure/type.ML	Tue Dec 30 21:48:07 2008 +0100
@@ -277,8 +277,9 @@
   let
     val fs = Term.fold_types (Term.fold_atyps
       (fn TFree v => if member (op =) fixed v then I else insert (op =) v | _ => I)) t [];
-    val ixns = add_term_tvar_ixns (t, []);
-    val fmap = fs ~~ map (rpair 0) (Name.variant_list (map #1 ixns) (map fst fs))
+    val used = Name.context
+      |> fold_types (fold_atyps (fn TVar ((a, _), _) => Name.declare a | _ => I)) t;
+    val fmap = fs ~~ map (rpair 0) (#1 (Name.variants (map fst fs) used));
     fun thaw (f as (a, S)) =
       (case AList.lookup (op =) fmap f of
         NONE => TFree f