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