1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Fri Dec 03 08:40:47 2010 +0100
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Fri Dec 03 08:40:47 2010 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4    val add : string option -> int option -> attribute
     1.5    val test_fn : (int * int * int -> term list option) Unsynchronized.ref
     1.6    val test_term:
     1.7 -    Proof.context -> term -> int -> term list option * (bool list * bool)
     1.8 +    Proof.context -> term -> int -> term list option * Quickcheck.report option
     1.9    val setup : theory -> theory
    1.10    val quickcheck_setup : theory -> theory
    1.11  end;
    1.12 @@ -842,10 +842,9 @@
    1.13      val start = Config.get ctxt depth_start;
    1.14      val offset = Config.get ctxt size_offset;
    1.15      val test_fn' = !test_fn;
    1.16 -    val dummy_report = ([], false)
    1.17      fun test k = (deepen bound (fn i =>
    1.18        (Output.urgent_message ("Search depth: " ^ string_of_int i);
    1.19 -       test_fn' (i, values, k+offset))) start, dummy_report);
    1.20 +       test_fn' (i, values, k+offset))) start, NONE);
    1.21    in test end;
    1.22  
    1.23  val quickcheck_setup =