--- a/src/HOL/Tools/Function/scnp_solve.ML Wed Oct 21 08:16:25 2009 +0200
+++ b/src/HOL/Tools/Function/scnp_solve.ML Wed Oct 21 10:15:31 2009 +0200
@@ -67,7 +67,7 @@
fun iexists n f = PropLogic.exists (map f (0 upto n - 1))
fun iforall2 n m f = all (map_product f (0 upto n - 1) (0 upto m - 1))
-fun the_one var n x = all (var x :: map (Not o var) ((0 upto n - 1) \\ [x]))
+fun the_one var n x = all (var x :: map (Not o var) (remove (op =) x (0 upto n - 1)))
fun exactly_one n f = iexists n (the_one f n)
(* SAT solving *)