--- a/src/HOL/Tools/Function/scnp_solve.ML Thu Oct 22 10:52:07 2009 +0200
+++ b/src/HOL/Tools/Function/scnp_solve.ML Thu Oct 22 13:48:06 2009 +0200
@@ -63,8 +63,8 @@
/ \ f i
0<=i<n
*)
-fun iforall n f = all (map f (0 upto n - 1))
-fun iexists n f = PropLogic.exists (map f (0 upto n - 1))
+fun iforall n f = all (map_range f n)
+fun iexists n f = PropLogic.exists (map_range f n)
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) (remove (op =) x (0 upto n - 1)))
@@ -221,7 +221,7 @@
let fun prog_pt_mapping p =
map_filter (fn x => if assign (P(p, x)) then SOME (x, assignTag p x) else NONE)
(0 upto (arity gp p) - 1)
- in map prog_pt_mapping (0 upto num_prog_pts gp - 1) end
+ in map_range prog_pt_mapping (num_prog_pts gp) end
val strict_list = filter (assign o STRICT) (0 upto num_graphs gp - 1)