deactivated timing of infering modes
authorbulwahn
Thu, 20 May 2010 07:34:45 +0200
changeset 37009 4ba91ea2bf6d
parent 37008 8da3b51726ac
child 37010 8096a4c755eb
deactivated timing of infering modes
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 19 18:24:09 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu May 20 07:34:45 2010 +0200
@@ -2824,7 +2824,7 @@
       prepare_intrs options compilation thy prednames (maps (intros_of ctxt) prednames)
     val _ = print_step options "Infering modes..."
     val ((moded_clauses, errors), thy') =
-      Output.cond_timeit true "Infering modes"
+      Output.cond_timeit (!Quickcheck.timing) "Infering modes"
       (fn _ => infer_modes mode_analysis_options
         options compilation preds all_modes param_vs clauses thy)
     val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses