diff -r 4384f4ae0574 -r 47cf4bc789aa src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Jun 09 17:46:25 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Thu Jun 09 17:51:49 2011 +0200
@@ -84,8 +84,8 @@
     val (argTs, resT) = strip_type (fastype_of func)
     val nctxt =
       Name.make_context (Term.fold_aterms (fn Free (x, _) => insert (op =) x | _ => I) (func $ pred) [])
-    val (argnames, nctxt') = Name.variants (replicate (length argTs) "a") nctxt
-    val ([resname], nctxt'') = Name.variants ["r"] nctxt'
+    val (argnames, nctxt') = fold_map Name.variant (replicate (length argTs) "a") nctxt
+    val (resname, nctxt'') = Name.variant "r" nctxt'
     val args = map Free (argnames ~~ argTs)
     val res = Free (resname, resT)
   in Logic.mk_equals