pervasive cond_timeit;

--- 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))