--- a/ProgTutorial/Essential.thy	Thu Apr 03 12:16:56 2014 +0100
+++ b/ProgTutorial/Essential.thy	Sun Apr 06 12:45:54 2014 +0100
@@ -178,7 +178,7 @@
   can use the following ML-function to set the printing depth to a higher 
   value:
 
-  @{ML [display,gray] "print_depth 50"}
+  @{ML [display,gray] "default_print_depth 50"}
   \end{exercise}
 
   The antiquotation @{text "@{prop \<dots>}"} constructs terms by inserting the