# HG changeset patch
# User bulwahn
# Date 1274333685 -7200
# Node ID 4ba91ea2bf6d4d70eeaef26c69732a120a4357cd
# Parent  8da3b51726aca52f5e474b3e587632e6f11e6df5
deactivated timing of infering modes

diff -r 8da3b51726ac -r 4ba91ea2bf6d 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