--- a/CookBook/Recipes/Timing.thy	Wed Mar 18 03:03:51 2009 +0100
+++ b/CookBook/Recipes/Timing.thy	Wed Mar 18 03:27:15 2009 +0100
@@ -27,7 +27,7 @@
   wrapper function:
 *}
 
-ML{*fun timing_wrapper tac st =
+ML %linenosgray{*fun timing_wrapper tac st =
 let 
   val t_start = start_timing ();
   val res = tac st;
@@ -38,7 +38,7 @@
 
 text {*
   Note that this function, in addition to a tactic, also takes a state @{text
-  "st"} as argument and applies this state to the tactic. The reason is that
+  "st"} as argument and applies this state to the tactic (Line 4). The reason is that
   tactics are lazy functions and you need to force them to run, otherwise the
   timing will be meaningless.  The time between start and finish of the tactic
   will be calculated as the end time minus the start time.  An example of the
@@ -53,7 +53,7 @@
 done
 
 text {*
-  where it returns something on the scale of 3 seconds. We choose to return
+  where it returns something on the scale of 3 seconds. We chose to return
   this information as a string, but the timing information is also accessible
   in number format.