src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Jun 09 17:46:25 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Jun 09 17:51:49 2011 +0200
@@ -542,7 +542,7 @@
 fun focus_ex t nctxt =
   let
     val ((xs, Ts), t') = apfst split_list (strip_ex t) 
-    val (xs', nctxt') = Name.variants xs nctxt;
+    val (xs', nctxt') = fold_map Name.variant xs nctxt;
     val ps' = xs' ~~ Ts;
     val vs = map Free ps';
     val t'' = Term.subst_bounds (rev vs, t');