diff -r e81ebb37aa83 -r b6fca043a796 CookBook/Recipes/TimeLimit.thy
--- a/CookBook/Recipes/TimeLimit.thy	Sun Mar 01 21:48:59 2009 +0000
+++ b/CookBook/Recipes/TimeLimit.thy	Mon Mar 02 10:06:06 2009 +0000
@@ -19,6 +19,8 @@
   | ackermann (m, 0) = ackermann (m - 1, 1)
   | ackermann (m, n) = ackermann (m - 1, ackermann (m, n - 1)) *}
 
+ML {* ackermann (3,4) *} 
+
 text {*
 
   Now the call