# HG changeset patch
# User blanchet
# Date 1458629821 -3600
# Node ID 1e5cf471e7030c25340d7487a35d5bd33365c151
# Parent  cb20e88281960b62fb3b0a7fa1a13edd13b136c2
added timers to N2M

diff -r cb20e8828196 -r 1e5cf471e703 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Mar 22 07:18:36 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Tue Mar 22 07:57:01 2016 +0100
@@ -249,6 +249,9 @@
           fp_bnf (construct_mutualized_fp fp mutual_cliques unsorted_fpTs fp_results) fp_bs
             unsorted_As' killed_As' fp_eqs no_defs_lthy;
 
+        val time = time lthy;
+        val timer = time (Timer.startRealTimer ());
+
         val fp_abs_inverses = map #abs_inverse fp_absT_infos;
         val fp_type_definitions = map #type_definition fp_absT_infos;
 
@@ -273,6 +276,8 @@
             fp_bs xtor_co_recs lthy
           |>> split_list;
 
+        val timer = time (timer ("High-level " ^ co_prefix fp ^ "recursors"));
+
         val ((common_co_inducts, co_inductss', co_rec_thmss, co_rec_disc_thmss, co_rec_sel_thmsss),
              fp_sugar_thms) =
           if fp = Least_FP then
@@ -294,6 +299,8 @@
                corec_disc_thmss, corec_sel_thmsss))
             ||> (fn info => (NONE, SOME info));
 
+        val timer = time (timer ("High-level " ^ co_prefix fp ^ "induction principles"));
+
         val names_lthy = lthy |> fold Variable.declare_typ (As @ Cs @ Xs);
         val phi = Proof_Context.export_morphism names_lthy lthy;
 
diff -r cb20e8828196 -r 1e5cf471e703 src/HOL/Tools/BNF/bnf_fp_util.ML
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Mar 22 07:18:36 2016 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Tue Mar 22 07:57:01 2016 +0100
@@ -276,7 +276,7 @@
 
 fun time ctxt timer msg = (if Config.get ctxt bnf_timing
   then warning (msg ^ ": " ^ string_of_int (Time.toMilliseconds (Timer.checkRealTimer timer)) ^
-    "ms")
+    " ms")
   else (); Timer.startRealTimer ());
 
 val preN = "pre_"