diff -r 4384f4ae0574 -r 47cf4bc789aa src/HOL/Nominal/nominal_primrec.ML
--- a/src/HOL/Nominal/nominal_primrec.ML	Thu Jun 09 17:46:25 2011 +0200
+++ b/src/HOL/Nominal/nominal_primrec.ML	Thu Jun 09 17:51:49 2011 +0200
@@ -36,7 +36,7 @@
   let
     val (vs, Ts) = split_list (strip_qnt_vars "all" t);
     val body = strip_qnt_body "all" t;
-    val (vs', _) = Name.variants vs (Name.make_context (fold_aterms
+    val (vs', _) = fold_map Name.variant vs (Name.make_context (fold_aterms
       (fn Free (v, _) => insert (op =) v | _ => I) body []))
   in (curry subst_bounds (map2 (curry Free) vs' Ts |> rev) body) end;