# HG changeset patch
# User bulwahn
# Date 1320861710 -3600
# Node ID aa35c9454a9569bc079ba03c3707a48667ebb913
# Parent  fca432074fb229cd31c9fb6f1ee610b7f811fbaa
quickcheck invocations in mutabelle must not catch codegenerator errors internally

diff -r fca432074fb2 -r aa35c9454a95 src/HOL/Mutabelle/mutabelle.ML
--- 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)
diff -r fca432074fb2 -r aa35c9454a95 src/HOL/Mutabelle/mutabelle_extra.ML
--- 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