diff -r 3c214b215f7e -r 77ea2de0ca62 ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Wed May 28 12:41:09 2014 +0100
+++ b/ProgTutorial/Essential.thy	Tue Jul 08 11:34:10 2014 +0100
@@ -175,12 +175,13 @@
 
   Hint: The third term is already quite big, and the pretty printer
   may omit parts of it by default. If you want to see all of it, you
-  can use the following ML-function to set the printing depth to a higher 
-  value:
-
-  @{ML [display,gray] "default_print_depth 50"}
+  need to set the printing depth to a higher value by 
   \end{exercise}
-
+*}
+
+declare [[ML_print_depth = 50]]
+
+text {*
   The antiquotation @{text "@{prop \<dots>}"} constructs terms by inserting the 
   usually invisible @{text "Trueprop"}-coercions whenever necessary. 
   Consider for example the pairs