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