# HG changeset patch
# User bulwahn
# Date 1271844653 -7200
# Node ID 01ccbaa3f49fa8815beb31792387758c4e183dca
# Parent  c0ab79a100e43338135e15ce5617bb58e8a9975b
make profiling depend on reference Quickcheck.timing

diff -r c0ab79a100e4 -r 01ccbaa3f49f src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Apr 21 12:10:52 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed Apr 21 12:10:53 2010 +0200
@@ -2824,18 +2824,18 @@
     val _ = print_modes options thy' modes
     val _ = print_step options "Defining executable functions..."
     val thy'' =
-      Output.cond_timeit true "Defining executable functions..."
+      Output.cond_timeit (!Quickcheck.timing) "Defining executable functions..."
       (fn _ => fold (#define_functions (dest_steps steps) options preds) modes thy'
       |> Theory.checkpoint)
     val _ = print_step options "Compiling equations..."
     val compiled_terms =
-      (*Output.cond_timeit true "Compiling equations...." (fn _ =>*)
+      Output.cond_timeit (!Quickcheck.timing) "Compiling equations...." (fn _ =>
         compile_preds options
-          (#comp_modifiers (dest_steps steps)) thy'' all_vs param_vs preds moded_clauses
+          (#comp_modifiers (dest_steps steps)) thy'' all_vs param_vs preds moded_clauses)
     val _ = print_compiled_terms options thy'' compiled_terms
     val _ = print_step options "Proving equations..."
     val result_thms =
-      Output.cond_timeit true "Proving equations...." (fn _ =>
+      Output.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) thy'' preds
       (maps_modes result_thms)
@@ -2843,7 +2843,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 true "Setting code equations...." (fn _ =>
+      Output.cond_timeit (!Quickcheck.timing) "Setting code equations...." (fn _ =>
       fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss
       [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms),
         [attrib thy ])] thy))