quickcheck invocations in mutabelle must not catch codegenerator errors internally

--- a/src/HOL/Mutabelle/mutabelle.ML	Wed Nov 09 17:57:42 2011 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML	Wed Nov 09 19:01:50 2011 +0100
@@ -496,7 +496,8 @@
     val ctxt' = Proof_Context.init_global thy
       |> Config.put Quickcheck.size 1
       |> Config.put Quickcheck.iterations 1
-    val test = Quickcheck_Common.test_term Exhaustive_Generators.compile_generator_expr ctxt' (true, false)
+    val test = Quickcheck_Common.test_term
+      ("exhaustive", Exhaustive_Generators.compile_generator_expr) ctxt' false
   in  
     case try test (preprocess thy insts (prop_of th), []) of
       SOME _ => (Output.urgent_message "executable"; true)

--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Nov 09 17:57:42 2011 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Wed Nov 09 19:01:50 2011 +0100
@@ -123,7 +123,7 @@
             val ctxt' = change_options (Proof_Context.init_global thy)
             val [result] = case Quickcheck.active_testers ctxt' of
               [] => error "No active testers for quickcheck"
-            | [tester] => tester ctxt' (false, false) [] [(t, [])]
+            | [tester] => tester ctxt' false [] [(t, [])]
             | _ => error "Multiple active testers for quickcheck"
           in
             case Quickcheck.counterexample_of result of