1.1 --- a/src/Tools/quickcheck.ML	Thu Dec 01 22:14:35 2011 +0100
     1.2 +++ b/src/Tools/quickcheck.ML	Thu Dec 01 22:14:35 2011 +0100
     1.3 @@ -39,16 +39,16 @@
     1.4    (* quickcheck's result *)
     1.5    datatype result =
     1.6      Result of
     1.7 -     {counterexample : (string * term) list option,
     1.8 +     {counterexample : (bool * (string * term) list) option,
     1.9        evaluation_terms : (term * term) list option,
    1.10        timings : (string * int) list,
    1.11        reports : (int * report) list}
    1.12    val empty_result : result
    1.13    val found_counterexample : result -> bool
    1.14    val add_timing : (string * int) -> result Unsynchronized.ref -> unit
    1.15 -  val add_response : string list -> term list -> term list option -> result Unsynchronized.ref -> unit
    1.16 +  val add_response : string list -> term list -> (bool * term list) option -> result Unsynchronized.ref -> unit
    1.17    val add_report : int -> report option -> result Unsynchronized.ref -> unit
    1.18 -  val counterexample_of : result -> (string * term) list option
    1.19 +  val counterexample_of : result -> (bool * (string * term) list) option
    1.20    val timings_of : result -> (string * int) list
    1.21    (* registering testers & generators *) 
    1.22    type tester =
    1.23 @@ -69,7 +69,7 @@
    1.24    val active_testers : Proof.context -> tester list
    1.25    val test_terms :
    1.26      Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list -> result list option
    1.27 -  val quickcheck: (string * string list) list -> int -> Proof.state -> (string * term) list option
    1.28 +  val quickcheck: (string * string list) list -> int -> Proof.state -> (bool * (string * term) list) option
    1.29  end;
    1.30  
    1.31  structure Quickcheck : QUICKCHECK =
    1.32 @@ -102,7 +102,7 @@
    1.33  (* Quickcheck Result *)
    1.34  
    1.35  datatype result = Result of
    1.36 -  { counterexample : (string * term) list option, evaluation_terms : (term * term) list option,
    1.37 +  { counterexample : (bool * (string * term) list) option, evaluation_terms : (term * term) list option,
    1.38      timings : (string * int) list, reports : (int * report) list}
    1.39  
    1.40  val empty_result =
    1.41 @@ -113,17 +113,18 @@
    1.42  fun found_counterexample (Result r) = is_some (#counterexample r)
    1.43  
    1.44  fun response_of (Result r) = case (#counterexample r, #evaluation_terms r) of
    1.45 -    (SOME ts, SOME evals) => SOME (ts, evals)
    1.46 +    (SOME (_, ts), SOME evals) => SOME (ts, evals)
    1.47    | (NONE, NONE) => NONE
    1.48  
    1.49  fun timings_of (Result r) = #timings r
    1.50  
    1.51 -fun set_response names eval_terms (SOME ts) (Result r) =
    1.52 +fun set_response names eval_terms (SOME (genuine, ts)) (Result r) =
    1.53    let
    1.54      val (ts1, ts2) = chop (length names) ts
    1.55      val (eval_terms', _) = chop (length ts2) eval_terms
    1.56    in
    1.57 -    Result {counterexample = SOME (names ~~ ts1), evaluation_terms = SOME (eval_terms' ~~ ts2),
    1.58 +    Result {counterexample = SOME (genuine, (names ~~ ts1)),
    1.59 +      evaluation_terms = SOME (eval_terms' ~~ ts2),
    1.60        timings = #timings r, reports = #reports r}
    1.61    end
    1.62    | set_response _ _ NONE result = result