# HG changeset patch
# User haftmann
# Date 1242306586 -7200
# Node ID 6b31b143f18b3bd6c44326d7ea68fcd100a24800
# Parent  e79d1ff2abc5635e3f6732f6bbf53383460f7916
quickcheck size starts with 0

diff -r e79d1ff2abc5 -r 6b31b143f18b src/HOL/Library/Quickcheck.thy
--- a/src/HOL/Library/Quickcheck.thy	Thu May 14 09:16:36 2009 +0200
+++ b/src/HOL/Library/Quickcheck.thy	Thu May 14 15:09:46 2009 +0200
@@ -75,7 +75,7 @@
     val tys = (map snd o fst o strip_abs) t;
     val t' = mk_generator_expr thy t tys;
     val f = Code_ML.eval (SOME target) ("Quickcheck.eval_ref", eval_ref)
-      (fn proc => fn g => fn s => g s #>> (Option.map o map) proc) thy t' [];
+      (fn proc => fn g => fn s => g (s + 1) #>> (Option.map o map) proc) thy t' [];
   in f #> Random_Engine.run end;
 
 end
diff -r e79d1ff2abc5 -r 6b31b143f18b src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Thu May 14 09:16:36 2009 +0200
+++ b/src/Pure/codegen.ML	Thu May 14 15:09:46 2009 +0200
@@ -329,7 +329,7 @@
   end;
 
 val assoc_const_i = gen_assoc_const (K I);
-val assoc_const = gen_assoc_const Code_Unit.read_bare_const;
+val assoc_const = gen_assoc_const Code.read_bare_const;
 
 
 (**** associate types with target language types ****)
@@ -889,7 +889,7 @@
           mk_let (map (fn ((s, T), s') =>
               (mk_tuple [str s', str (s' ^ "_t")],
                Pretty.block [mk_gen gr "Generated" false [] "" T, Pretty.brk 1,
-                 str "(i + 1)"])) frees')
+                 str "i"])) frees')
             (Pretty.block [str "if ",
               mk_app false (str "testf") (map (str o snd) frees'),
               Pretty.brk 1, str "then NONE",
diff -r e79d1ff2abc5 -r 6b31b143f18b src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Thu May 14 09:16:36 2009 +0200
+++ b/src/Tools/quickcheck.ML	Thu May 14 15:09:46 2009 +0200
@@ -104,12 +104,12 @@
      of NONE => if quiet then mk_testers ctxt t' else mk_testers_strict ctxt t'
       | SOME name => [mk_tester_select name ctxt t'];
     fun iterate f 0 = NONE
-      | iterate f k = case f () handle Match => (if quiet then ()
+      | iterate f j = case f () handle Match => (if quiet then ()
              else warning "Exception Match raised during quickcheck"; NONE)
-          of NONE => iterate f (k - 1) | SOME q => SOME q;
+          of NONE => iterate f (j - 1) | SOME q => SOME q;
     fun with_testers k [] = NONE
       | with_testers k (tester :: testers) =
-          case iterate (fn () => tester k) i
+          case iterate (fn () => tester (k - 1)) i
            of NONE => with_testers k testers
             | SOME q => SOME q;
     fun with_size k = if k > size then NONE