--- a/ProgTutorial/Recipes/Timing.thy	Fri Mar 18 02:53:14 2011 +0100
+++ b/ProgTutorial/Recipes/Timing.thy	Thu Apr 07 00:25:26 2011 +0100
@@ -9,7 +9,7 @@
   You want to measure the running time of a tactic or function.\smallskip
 
   {\bf Solution:} Time can be measured using the function 
-  @{ML start_timing} and @{ML end_timing}.\smallskip
+  @{ML start in Timing} and @{ML result in Timing}.\smallskip
 
   Suppose you defined the Ackermann function on the Isabelle level. 
 *}
@@ -29,11 +29,11 @@
 
 ML %linenosgray{*fun timing_wrapper tac st =
 let 
-  val t_start = start_timing ();
+  val t_start = Timing.start ();
   val res = tac st;
-  val t_end = end_timing t_start;
+  val t_end = Timing.result t_start;
 in
-  (writeln (#message t_end); res)
+  (writeln (Timing.message t_end); res)
 end*}
 
 text {*
@@ -62,7 +62,7 @@
 
   \begin{readmore}
   Basic functions regarding timing are defined in @{ML_file 
-  "Pure/ML-Systems/polyml_common.ML"} (for the PolyML compiler). Some more
+  "Pure/General/timing.ML"} (for the PolyML compiler). Some more
   advanced functions are defined in @{ML_file "Pure/General/output.ML"}.
   \end{readmore}
 *}

Binary file progtutorial.pdf has changed