1.1 --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Dec 01 22:14:35 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML	Thu Dec 01 22:14:35 2011 +0100
     1.3 @@ -489,8 +489,7 @@
     1.4        thy (SOME target) (K I) (HOLogic.mk_list @{typ "code_numeral => bool"} ts') []
     1.5    end;
     1.6  
     1.7 -val test_goals = Quickcheck_Common.generator_test_goal_terms ("exhaustive",
     1.8 -  apfst (Option.map snd) ooo compile_generator_expr);
     1.9 +val test_goals = Quickcheck_Common.generator_test_goal_terms ("exhaustive", compile_generator_expr);
    1.10    
    1.11  (* setup *)
    1.12  

     2.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Dec 01 22:14:35 2011 +0100
     2.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Dec 01 22:14:35 2011 +0100
     2.3 @@ -437,7 +437,7 @@
     2.4            thy (apfst o Option.map o map_counterexample) (mk_property qs prop_t)
     2.5        in
     2.6          Quickcheck.Result
     2.7 -         {counterexample = Option.map (mk_terms ctxt qs) counterexample,
     2.8 +         {counterexample = Option.map (pair true o mk_terms ctxt qs) counterexample,
     2.9            evaluation_terms = Option.map (K []) counterexample,
    2.10            timings = #timings (dest_result result), reports = #reports (dest_result result)}
    2.11        end
    2.12 @@ -454,7 +454,7 @@
    2.13        in
    2.14          Quickcheck.Result
    2.15           {counterexample =
    2.16 -           Option.map (((curry (op ~~)) (Term.add_free_names t [])) o map post_process o snd) counterexample,
    2.17 +           Option.map (apsnd (((curry (op ~~)) (Term.add_free_names t [])) o map post_process)) counterexample,
    2.18            evaluation_terms = Option.map (K []) counterexample,
    2.19            timings = #timings (dest_result result), reports = #reports (dest_result result)}
    2.20        end

     3.1 --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Dec 01 22:14:35 2011 +0100
     3.2 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Thu Dec 01 22:14:35 2011 +0100
     3.3 @@ -17,7 +17,7 @@
     3.4    val mk_safe_if : Proof.context -> term * term * (bool -> term) -> term
     3.5    val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list
     3.6    type compile_generator =
     3.7 -    Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
     3.8 +    Proof.context -> (term * term list) list -> int list -> (bool * term list) option * Quickcheck.report option
     3.9    val generator_test_goal_terms :
    3.10      string * compile_generator -> Proof.context -> bool -> (string * typ) list
    3.11      -> (term * term list) list -> Quickcheck.result list
    3.12 @@ -53,7 +53,7 @@
    3.13  (* testing functions: testing with increasing sizes (and cardinalities) *)
    3.14  
    3.15  type compile_generator =
    3.16 -  Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
    3.17 +  Proof.context -> (term * term list) list -> int list -> (bool * term list) option * Quickcheck.report option
    3.18  
    3.19  fun check_test_term t =
    3.20    let

     4.1 --- a/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Dec 01 22:14:35 2011 +0100
     4.2 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML	Thu Dec 01 22:14:35 2011 +0100
     4.3 @@ -11,7 +11,7 @@
     4.4      -> (seed -> ('b * (unit -> term)) * seed) -> (seed -> seed * seed)
     4.5      -> seed -> (('a -> 'b) * (unit -> term)) * seed
     4.6    val compile_generator_expr:
     4.7 -    Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
     4.8 +    Proof.context -> (term * term list) list -> int list -> (bool * term list) option * Quickcheck.report option
     4.9    val put_counterexample: (unit -> int -> int -> seed -> (bool * term list) option * seed)
    4.10      -> Proof.context -> Proof.context
    4.11    val put_counterexample_report: (unit -> int -> int -> seed -> (term list option * (bool list * bool)) * seed)
    4.12 @@ -417,7 +417,7 @@
    4.13                val report = collect_single_report single_report report
    4.14              in
    4.15                case test_result of NONE => iterate_and_collect (card, size) (j - 1) report
    4.16 -                | SOME q => (SOME q, report)
    4.17 +                | SOME q => (SOME (true, q), report)
    4.18              end
    4.19        in
    4.20          fn [card, size] => apsnd SOME (iterate_and_collect (card, size) iterations empty_report)
    4.21 @@ -429,7 +429,7 @@
    4.22            (Counterexample.get, put_counterexample, "Random_Generators.put_counterexample")
    4.23            thy (SOME target)
    4.24            (fn proc => fn g => fn c => fn s =>g c s #>> (Option.map o apsnd o map) proc) t' [];
    4.25 -        fun single_tester c s = compile c s |> Random_Engine.run |> Option.map snd
    4.26 +        fun single_tester c s = compile c s |> Random_Engine.run
    4.27          fun iterate (card, size) 0 = NONE
    4.28            | iterate (card, size) j =
    4.29              case single_tester card size of NONE => iterate (card, size) (j - 1) | SOME q => SOME q