1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Jun 09 15:38:49 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Jun 09 16:34:49 2011 +0200
     1.3 @@ -849,7 +849,7 @@
     1.4        |>> (introduce_proxies format type_sys #> AAtom)
     1.5        ||> union (op =) atomic_types
     1.6      fun do_quant bs q s T t' =
     1.7 -      let val s = Name.variant (map fst bs) s in
     1.8 +      let val s = singleton (Name.variant_list (map fst bs)) s in
     1.9          do_formula ((s, T) :: bs) t'
    1.10          #>> mk_aquant q [(`make_bound_var s, SOME T)]
    1.11        end