--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Jun 09 15:38:49 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Jun 09 16:34:49 2011 +0200
@@ -155,7 +155,7 @@
fun close_form t =
(t, [] |> Term.add_free_names t |> maps all_prefixes_of)
|> fold (fn ((s, i), T) => fn (t', taken) =>
- let val s' = Name.variant taken s in
+ let val s' = singleton (Name.variant_list taken) s in
((if fastype_of t' = HOLogic.boolT then HOLogic.all_const
else Term.all) T
$ Abs (s', T, abstract_over (Var ((s, i), T), t')),