CookBook/Recipes/TimeLimit.thy
changeset 102 5e309df58557
parent 94 531e453c9d67
child 155 b6fca043a796
--- 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,