--- a/src/HOL/Library/SML_Quickcheck.thy Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Library/SML_Quickcheck.thy Fri Dec 03 08:40:47 2010 +0100
@@ -7,7 +7,21 @@
setup {*
Inductive_Codegen.quickcheck_setup #>
- Context.theory_map (Quickcheck.add_generator ("SML", Codegen.test_term))
+ Context.theory_map (Quickcheck.add_generator ("SML",
+ fn ctxt => fn t =>
+ let
+ val test_fun = Codegen.test_term ctxt t
+ val iterations = Config.get ctxt Quickcheck.iterations
+ fun iterate size 0 = NONE
+ | iterate size j =
+ let
+ val result = test_fun size handle Match =>
+ (if Config.get ctxt Quickcheck.quiet then ()
+ else warning "Exception Match raised during quickcheck"; NONE)
+ in
+ case result of NONE => iterate size (j - 1) | SOME q => SOME q
+ end
+ in fn size => (iterate size iterations, NONE) end))
*}
end
--- a/src/Pure/codegen.ML Fri Dec 03 08:40:47 2010 +0100
+++ b/src/Pure/codegen.ML Fri Dec 03 08:40:47 2010 +0100
@@ -76,7 +76,7 @@
val mk_term_of: codegr -> string -> bool -> typ -> Pretty.T
val mk_gen: codegr -> string -> bool -> string list -> string -> typ -> Pretty.T
val test_fn: (int -> term list option) Unsynchronized.ref
- val test_term: Proof.context -> term -> int -> term list option * (bool list * bool)
+ val test_term: Proof.context -> term -> int -> term list option
val eval_result: (unit -> term) Unsynchronized.ref
val eval_term: theory -> term -> term
val evaluation_conv: cterm -> thm
@@ -895,8 +895,7 @@
str ");"]) ^
"\n\nend;\n";
val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;
- val dummy_report = ([], false)
- in (fn size => (! test_fn size, dummy_report)) end;
+ in (fn size => (! test_fn size)) end;