# HG changeset patch
# User boehmes
# Date 1251901790 -7200
# Node ID 922718ac81e419e5cc0d66765662f6e0777579d8
# Parent  4ab00a2642c3fc1139625090a072e32fcdc270b7
removed errors overseen in previous changes

diff -r 4ab00a2642c3 -r 922718ac81e4 src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Wed Sep 02 16:23:53 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Wed Sep 02 16:29:50 2009 +0200
@@ -29,7 +29,7 @@
 
 
 
-structure Mirabelle : MIRABELLE_EXT =
+structure Mirabelle : MIRABELLE =
 struct
 
 (* Mirabelle configuration *)
diff -r 4ab00a2642c3 -r 922718ac81e4 src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Wed Sep 02 16:23:53 2009 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Wed Sep 02 16:29:50 2009 +0200
@@ -5,14 +5,14 @@
 structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
 struct
 
-fun quickcheck_action limit args {pre=st, ...} =
+fun quickcheck_action args {pre, timeout, log, ...} =
   let
     val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
     val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1
   in
-    (case TimeLimit.timeLimit limit quickcheck st of
-      NONE => SOME "no counterexample"
-    | SOME _ => SOME "counterexample found")
+    (case TimeLimit.timeLimit timeout quickcheck pre of
+      NONE => log "no counterexample"
+    | SOME _ => log "counterexample found")
   end
 
 fun invoke args = Mirabelle.register ("quickcheck", quickcheck_action args)