# HG changeset patch
# User wenzelm
# Date 1193249870 -7200
# Node ID b84f3c3c27f245ac2b5f6ab51976c6b7b9532410
# Parent  1cd45207dd3f03d33dbc3afbcaca148f390b8f2c
separate RecordPackage.timing flag;

diff -r 1cd45207dd3f -r b84f3c3c27f2 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed Oct 24 20:17:48 2007 +0200
+++ b/src/HOL/Tools/record_package.ML	Wed Oct 24 20:17:50 2007 +0200
@@ -25,6 +25,7 @@
 sig
   include BASIC_RECORD_PACKAGE
   val quiet_mode: bool ref
+  val timing: bool ref
   val record_quick_and_dirty_sensitive: bool ref
   val updateN: string
   val updN: string
@@ -121,6 +122,7 @@
 
 (* timing *)
 
+val timing = ref false;
 fun timeit_msg s x = if !timing then (warning s; timeit x) else x ();
 fun timing_msg s = if !timing then warning s else ();