removed errors overseen in previous changes

--- 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 *)

--- 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)