--- 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;