configuration option to control timing output for (co)datatypes

--- a/src/HOL/BNF/Tools/bnf_def.ML	Thu Aug 22 16:03:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Thu Aug 22 17:13:46 2013 +0200
@@ -89,6 +89,7 @@
   datatype fact_policy = Dont_Note | Note_Some | Note_All
 
   val bnf_note_all: bool Config.T
+  val bnf_timing: bool Config.T
   val user_policy: fact_policy -> Proof.context -> fact_policy
   val note_bnf_thms: fact_policy -> (binding -> binding) -> binding -> bnf -> Proof.context ->
     Proof.context
@@ -532,6 +533,7 @@
 datatype fact_policy = Dont_Note | Note_Some | Note_All;
 
 val bnf_note_all = Attrib.setup_config_bool @{binding bnf_note_all} (K false);
+val bnf_timing = Attrib.setup_config_bool @{binding bnf_timing} (K false);
 
 fun user_policy policy ctxt = if Config.get ctxt bnf_note_all then Note_All else policy;
 

--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 22 16:03:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu Aug 22 17:13:46 2013 +0200
@@ -1115,6 +1115,7 @@
       fp_bnf (construct_fp mixfixes map_bs rel_bs set_bss) fp_bs (map dest_TFree unsorted_As) fp_eqs
         no_defs_lthy0;
 
+    val time = time lthy;
     val timer = time (Timer.startRealTimer ());
 
     val nesting_bnfs = nesty_bnfs lthy ctrXs_Tsss As;

--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu Aug 22 16:03:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu Aug 22 17:13:46 2013 +0200
@@ -33,7 +33,7 @@
   val un_fold_of: 'a list -> 'a
   val co_rec_of: 'a list -> 'a
 
-  val time: Timer.real_timer -> string -> Timer.real_timer
+  val time: Proof.context -> Timer.real_timer -> string -> Timer.real_timer
 
   val IITN: string
   val LevN: string
@@ -240,8 +240,8 @@
 fun un_fold_of [f, _] = f;
 fun co_rec_of [_, r] = r;
 
-val timing = true;
-fun time timer msg = (if timing
+
+fun time ctxt timer msg = (if Config.get ctxt bnf_timing
   then warning (msg ^ ": " ^ ATP_Util.string_of_time (Timer.checkRealTimer timer))
   else (); Timer.startRealTimer ());
 
@@ -573,6 +573,7 @@
 
 fun fp_bnf construct_fp bs resBs eqs lthy =
   let
+    val time = time lthy;
     val timer = time (Timer.startRealTimer ());
     val (lhss, rhss) = split_list eqs;
 

--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Aug 22 16:03:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu Aug 22 17:13:46 2013 +0200
@@ -57,6 +57,7 @@
 (*all BNFs have the same lives*)
 fun construct_gfp mixfixes map_bs rel_bs set_bss bs resBs (resDs, Dss) bnfs lthy =
   let
+    val time = time lthy;
     val timer = time (Timer.startRealTimer ());
 
     val live = live_of_bnf (hd bnfs);

--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Aug 22 16:03:13 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu Aug 22 17:13:46 2013 +0200
@@ -28,6 +28,7 @@
 (*all BNFs have the same lives*)
 fun construct_lfp mixfixes map_bs rel_bs set_bss bs resBs (resDs, Dss) bnfs lthy =
   let
+    val time = time lthy;
     val timer = time (Timer.startRealTimer ());
 
     val live = live_of_bnf (hd bnfs);