--- a/src/HOL/Tools/Predicate_Compile/mode_inference.ML Sun Mar 20 20:20:41 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/mode_inference.ML Sun Mar 20 21:20:07 2011 +0100
@@ -527,10 +527,10 @@
val rs = these (AList.lookup (op =) clauses p)
fun check_mode m =
let
- val res = Output.cond_timeit false "work part of check_mode for one mode" (fn _ =>
+ val res = cond_timeit false "work part of check_mode for one mode" (fn _ =>
map (check_mode_clause' mode_analysis_options thy p param_vs modes m) rs)
in
- Output.cond_timeit false "aux part of check_mode for one mode" (fn _ =>
+ cond_timeit false "aux part of check_mode for one mode" (fn _ =>
case find_indices is_none res of
[] => Success (exists (fn SOME (_, _, true) => true | _ => false) res)
| is => (print_failed_mode options thy modes p m rs is; Error (error_of p m is)))
@@ -538,7 +538,7 @@
val _ = if show_mode_inference options then
tracing ("checking " ^ string_of_int (length ms) ^ " modes ...")
else ()
- val res = Output.cond_timeit false "check_mode" (fn _ => map (fn (m, _) => (m, check_mode m)) ms)
+ val res = cond_timeit false "check_mode" (fn _ => map (fn (m, _) => (m, check_mode m)) ms)
val (ms', errors) = split res
in
((p, (ms' : ((bool * mode) * bool) list)), errors)
@@ -622,7 +622,7 @@
(check_modes_pred' mode_analysis_options options ctxt param_vs clauses
(modes @ extra_modes)) modes
val ((modes : (string * ((bool * mode) * bool) list) list), errors) =
- Output.cond_timeit false "Fixpount computation of mode analysis" (fn () =>
+ cond_timeit false "Fixpount computation of mode analysis" (fn () =>
if show_invalid_clauses options then
fixp_with_state (fn (modes, errors) =>
let
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sun Mar 20 20:20:41 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sun Mar 20 21:20:07 2011 +0100
@@ -130,12 +130,12 @@
fun preprocess options t thy =
let
val _ = print_step options "Fetching definitions from theory..."
- val gr = Output.cond_timeit (!Quickcheck.timing) "preprocess-obtain graph"
+ val gr = cond_timeit (!Quickcheck.timing) "preprocess-obtain graph"
(fn () => Predicate_Compile_Data.obtain_specification_graph options thy t
|> (fn gr => Term_Graph.subgraph (member (op =) (Term_Graph.all_succs gr [t])) gr))
val _ = if !present_graph then Predicate_Compile_Data.present_graph gr else ()
in
- Output.cond_timeit (!Quickcheck.timing) "preprocess-process"
+ cond_timeit (!Quickcheck.timing) "preprocess-process"
(fn () => (fold_rev (preprocess_strong_conn_constnames options gr)
(Term_Graph.strong_conn gr) thy))
end
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Mar 20 20:20:41 2011 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Mar 20 21:20:07 2011 +0100
@@ -1363,7 +1363,7 @@
val (lookup_mode, lookup_neg_mode, needs_random) = (modes_of compilation ctxt,
modes_of (negative_compilation_of compilation) ctxt, needs_random ctxt)
val ((moded_clauses, needs_random), errors) =
- Output.cond_timeit (!Quickcheck.timing) "Infering modes"
+ cond_timeit (!Quickcheck.timing) "Infering modes"
(fn _ => infer_modes mode_analysis_options
options (lookup_mode, lookup_neg_mode, needs_random) ctxt preds all_modes param_vs clauses)
val thy' = fold (fn (s, ms) => set_needs_random s ms) needs_random thy
@@ -1373,19 +1373,19 @@
val _ = print_modes options modes
val _ = print_step options "Defining executable functions..."
val thy'' =
- Output.cond_timeit (!Quickcheck.timing) "Defining executable functions..."
+ cond_timeit (!Quickcheck.timing) "Defining executable functions..."
(fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy'
|> Theory.checkpoint)
val ctxt'' = ProofContext.init_global thy''
val _ = print_step options "Compiling equations..."
val compiled_terms =
- Output.cond_timeit (!Quickcheck.timing) "Compiling equations...." (fn _ =>
+ cond_timeit (!Quickcheck.timing) "Compiling equations...." (fn _ =>
compile_preds options
(#comp_modifiers (dest_steps steps)) ctxt'' all_vs param_vs preds moded_clauses)
val _ = print_compiled_terms options ctxt'' compiled_terms
val _ = print_step options "Proving equations..."
val result_thms =
- Output.cond_timeit (!Quickcheck.timing) "Proving equations...." (fn _ =>
+ cond_timeit (!Quickcheck.timing) "Proving equations...." (fn _ =>
#prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms)
val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds
(maps_modes result_thms)
@@ -1393,7 +1393,7 @@
val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute
(fn thm => Context.mapping (Code.add_eqn thm) I))))
val thy''' =
- Output.cond_timeit (!Quickcheck.timing) "Setting code equations...." (fn _ =>
+ cond_timeit (!Quickcheck.timing) "Setting code equations...." (fn _ =>
fold (fn (name, result_thms) => fn thy => snd (Global_Theory.add_thmss
[((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms),
[attrib thy ])] thy))