diff -r 8629581acc0b -r 594890623c46 src/HOL/Tools/Mirabelle/Tools/mirabelle_quickcheck.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Tools/Mirabelle/Tools/mirabelle_quickcheck.ML	Fri Aug 21 13:21:19 2009 +0200
@@ -0,0 +1,19 @@
+(* Title:  mirabelle_quickcheck.ML
+   Author: Jasmin Blanchette and Sascha Boehme
+*)
+
+structure Mirabelle_Quickcheck : MIRABELLE_ACTION =
+struct
+
+fun quickcheck_action args {pre=st, ...} =
+  let
+    val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
+  in
+    (case Quickcheck.quickcheck (filter has_valid_key args) 1 st of
+      NONE => SOME "no counterexample"
+    | SOME _ => SOME "counterexample found")
+  end
+
+fun invoke args = Mirabelle.register ("quickcheck", quickcheck_action args)
+
+end