diff -r 638ed040e6f8 -r 2c34c69236ce ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Thu Apr 03 12:16:56 2014 +0100
+++ b/ProgTutorial/Parsing.thy	Sun Apr 06 12:45:54 2014 +0100
@@ -561,7 +561,7 @@
 end" 
 "([\"}\", \"{\", \<dots>], [\"\<rightleftharpoons>\", \"\<leftharpoondown>\", \<dots>])"}
 
-  You might have to adjust the @{ML_ind print_depth} in order to
+  You might have to adjust the @{ML_ind default_print_depth} in order to
   see the complete list.
 
   The parser @{ML_ind "$$$" in Parse} parses a single keyword. For example: