# HG changeset patch
# User bulwahn
# Date 1327997187 -3600
# Node ID 110ba63444462cfdc528c348cf35cabdca7ce01b
# Parent  d724066ff3d01a64fd9f3b0aba678d141d06cd20
mutabelle must handle the case where quickcheck returns multiple results

diff -r d724066ff3d0 -r 110ba6344446 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Jan 31 08:52:47 2012 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Tue Jan 31 09:06:27 2012 +0100
@@ -121,7 +121,7 @@
       (fn _ =>
           let
             val ctxt' = change_options (Proof_Context.init_global thy)
-            val [result] = case Quickcheck.active_testers ctxt' of
+            val (result :: _) = case Quickcheck.active_testers ctxt' of
               [] => error "No active testers for quickcheck"
             | [tester] => tester ctxt' false [] [(t, [])]
             | _ => error "Multiple active testers for quickcheck"