src/HOL/Tools/Quickcheck/quickcheck_common.ML

   val instantiate_goals: Proof.context -> (string * typ) list -> (term * term list) list
     -> (typ option * (term * term list)) list list
   val mk_safe_if : Proof.context -> term * term * (bool -> term) -> term
   val collect_results : ('a -> Quickcheck.result) -> 'a list -> Quickcheck.result list -> Quickcheck.result list
   type compile_generator =
-    Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
+    Proof.context -> (term * term list) list -> int list -> (bool * term list) option * Quickcheck.report option
   val generator_test_goal_terms :
     string * compile_generator -> Proof.context -> bool -> (string * typ) list
     -> (term * term list) list -> Quickcheck.result list
   val ensure_sort_datatype:
     ((sort * sort) * sort) * (Datatype.config -> Datatype.descr -> (string * sort) list

 fun mk_undefined T = Const(@{const_name undefined}, T)
 
 (* testing functions: testing with increasing sizes (and cardinalities) *)
 
 type compile_generator =
-  Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option
+  Proof.context -> (term * term list) list -> int list -> (bool * term list) option * Quickcheck.report option
 
 fun check_test_term t =
   let
     val _ = (null (Term.add_tvars t []) andalso null (Term.add_tfrees t [])) orelse
       error "Term to be tested contains type variables";