1.1 --- a/src/Pure/drule.ML	Thu Jun 09 15:38:49 2011 +0200
     1.2 +++ b/src/Pure/drule.ML	Thu Jun 09 16:34:49 2011 +0200
     1.3 @@ -337,7 +337,7 @@
     1.4         [] => (fth, fn x => x)
     1.5       | vars =>
     1.6           let fun newName (Var(ix,_), (pairs,used)) =
     1.7 -                   let val v = Name.variant used (string_of_indexname ix)
     1.8 +                   let val v = singleton (Name.variant_list used) (string_of_indexname ix)
     1.9                     in  ((ix,v)::pairs, v::used)  end;
    1.10               val (alist, _) = List.foldr newName ([], Library.foldr OldTerm.add_term_names
    1.11                 (prop :: Thm.terms_of_tpairs tpairs, [])) vars