# 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;