# HG changeset patch
# User bulwahn
# Date 1291362047 -3600
# Node ID b5a319668955af52fdf766c33fad4c8367c6ba8b
# Parent  647142607448063da8757cdccc5039bb10f55b42
adapting mutabelle

diff -r 647142607448 -r b5a319668955 src/HOL/Mutabelle/mutabelle.ML
--- a/src/HOL/Mutabelle/mutabelle.ML	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML	Fri Dec 03 08:40:47 2010 +0100
@@ -497,9 +497,9 @@
  (map_types (inst_type insts) (freeze t));
 
 fun is_executable thy insts th =
-  ((Quickcheck.test_term
+  ((Quickcheck.test_term 
       ((Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) (ProofContext.init_global thy))
-      (SOME (!testgen_name)) (preprocess thy insts (prop_of th));
+      false (SOME (!testgen_name)) (preprocess thy insts (prop_of th));
     Output.urgent_message "executable"; true) handle ERROR s =>
     (Output.urgent_message ("not executable: " ^ s); false));
 
@@ -509,7 +509,7 @@
      ((x, pretty (the_default [] (fst (Quickcheck.test_term
        ((Config.put Quickcheck.size sz #> Config.put Quickcheck.iterations qciter)
          (ProofContext.init_global usedthy))
-       (SOME (!testgen_name)) (preprocess usedthy insts x))))) :: acc))
+       false (SOME (!testgen_name)) (preprocess usedthy insts x))))) :: acc))
           handle ERROR msg => (Output.urgent_message msg; qc_recursive usedthy xs insts sz qciter acc);
 
 
diff -r 647142607448 -r b5a319668955 src/HOL/Mutabelle/mutabelle_extra.ML
--- a/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle_extra.ML	Fri Dec 03 08:40:47 2010 +0100
@@ -117,7 +117,7 @@
   TimeLimit.timeLimit (Time.fromSeconds (!Auto_Tools.time_limit))
       (fn _ =>
           case Quickcheck.test_goal_terms (change_options (ProofContext.init_global thy))
-              (SOME quickcheck_generator, []) [t] of
+              false (SOME quickcheck_generator, []) [t] of
             (NONE, _) => (NoCex, ([], NONE))
           | (SOME _, _) => (GenuineCex, ([], NONE))) ()
   handle TimeLimit.TimeOut => (Timeout, ([("timelimit", !Auto_Tools.time_limit)], NONE))
@@ -331,7 +331,7 @@
       (Quickcheck.test_goal_terms
         ((Config.put Quickcheck.finite_types true #>
           Config.put Quickcheck.size 1 #> Config.put Quickcheck.iterations 1) ctxt)
-        (SOME "random" , []))) (map (Object_Logic.atomize_term thy) (fst (Variable.import_terms true [t] ctxt)))
+        false (SOME "random" , []))) (map (Object_Logic.atomize_term thy) (fst (Variable.import_terms true [t] ctxt)))
   end
 
 fun is_executable_thm thy th = is_executable_term thy (prop_of th)
diff -r 647142607448 -r b5a319668955 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Fri Dec 03 08:40:47 2010 +0100
+++ b/src/Tools/quickcheck.ML	Fri Dec 03 08:40:47 2010 +0100
@@ -260,7 +260,7 @@
          (fn result => case result of NONE => NONE
         | SOME ts => SOME (names ~~ ts)) (with_size 1 []))) ()
       handle TimeLimit.TimeOut =>
-        if is_interactive then error (excipit "ran out of time") else TimeLimit.TimeOut
+        if is_interactive then error (excipit "ran out of time") else raise TimeLimit.TimeOut
   in
     (result, ([exec_time, comp_time], if Config.get ctxt report then SOME reports else NONE))
   end;