src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML
changeset 61140 78ece168f5b5
parent 59154 68ca25931dce
child 69593 3dda49e08b9d
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Sun Sep 06 22:14:52 2015 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML	Wed Sep 09 17:07:44 2015 +0200
@@ -26,7 +26,7 @@
   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