# HG changeset patch
# User bulwahn
# Date 1279728711 -7200
# Node ID 581c1e5f53e0758e4e98278e610d82e360b69d97
# Parent  88aba1803b3549e49072547cb2fe0e5625cb506f
fixing quickcheck invocation in HOL-Mirabelle

diff -r 88aba1803b35 -r 581c1e5f53e0 src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Wed Jul 21 18:11:51 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_quickcheck.ML	Wed Jul 21 18:11:51 2010 +0200
@@ -13,7 +13,7 @@
 fun run args id ({pre, timeout, log, ...}: Mirabelle.run_args) =
   let
     val has_valid_key = member (op =) ["iterations", "size", "generator"] o fst
-    val quickcheck = Quickcheck.quickcheck (filter has_valid_key args) 1
+    val quickcheck = Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key args)) 1
   in
     (case TimeLimit.timeLimit timeout quickcheck pre of
       NONE => log (qc_tag id ^ "no counterexample")