diff -r 542b34b178ec -r 4d462963a7db src/HOL/Tools/Function/scnp_solve.ML
--- 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)