src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML

     (unit -> Code_Numeral.natural -> term list Lazy_Sequence.lazy_sequence) ->
     Proof.context -> Proof.context
   val put_cps_result : (unit -> Code_Numeral.natural -> (bool * term list) option) ->
     Proof.context -> Proof.context
   val test_goals : (Predicate_Compile_Aux.compilation * bool) ->
-    Proof.context -> bool * bool -> (string * typ) list -> (term * term list) list ->
+    Proof.context -> bool -> (string * typ) list -> (term * term list) list ->
     Quickcheck.result list
   val nrandom : int Unsynchronized.ref
   val debug : bool Unsynchronized.ref
   val no_higher_order_predicate : string list Unsynchronized.ref
 end;