diff -r 123401a5c8e9 -r 5e309df58557 CookBook/Recipes/TimeLimit.thy
--- a/CookBook/Recipes/TimeLimit.thy	Fri Feb 06 06:19:52 2009 +0000
+++ b/CookBook/Recipes/TimeLimit.thy	Sat Feb 07 12:05:02 2009 +0000
@@ -33,7 +33,7 @@
   handle TimeLimit.TimeOut => ~1"
 "~1"}
 
-  where @{ML_text TimeOut} is the exception raised when the time limit
+  where @{text TimeOut} is the exception raised when the time limit
   is reached.
 
   Note that @{ML  "timeLimit" in TimeLimit} is only meaningful when you use PolyML,