--- a/ProgTutorial/Advanced.thy	Thu Nov 10 15:54:13 2011 +0000
+++ b/ProgTutorial/Advanced.thy	Thu Nov 10 16:06:17 2011 +0000
@@ -257,6 +257,22 @@
   Now let us come back to the point about printing terms.
 *}
 
+ML {*
+let
+  val trm = @{term "x y z w"}
+in
+  pwriteln (Pretty.chunks 
+    [ pretty_term ctxt0 trm,
+      pretty_term ctxt1 trm,
+      pretty_term ctxt2 trm ])
+end
+*}
+
+
+text {*
+  
+*}
+
 
 (*
 ML{*Proof_Context.debug := true*}