# HG changeset patch
# User bulwahn
# Date 1291362047 -3600
# Node ID cdb34f393a7ef45b89fbe67fdb81513842863a28
# Parent  7351c6afb34875c5161c6468472d6093272ea084
adapting SML_Quickcheck to recent changes

diff -r 7351c6afb348 -r cdb34f393a7e src/HOL/Library/SML_Quickcheck.thy
--- 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
diff -r 7351c6afb348 -r cdb34f393a7e src/Pure/codegen.ML
--- 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;