diff -r 14173c0e8688 -r 2ac9dc1a95b4 ProgTutorial/FirstSteps.thy
--- a/ProgTutorial/FirstSteps.thy	Wed Aug 05 08:58:28 2009 +0200
+++ b/ProgTutorial/FirstSteps.thy	Wed Aug 05 09:24:18 2009 +0200
@@ -267,6 +267,18 @@
 fun string_of_thms_no_vars ctxt thms =  
   commas (map (string_of_thm_no_vars ctxt) thms) *}
 
+text {*
+  When printing out several `parcels' of information that belong 
+  together you should try to keep this information together. For 
+  this you can use the function @{ML [index] cat_lines}, which 
+  concatenates a list of strings and inserts newlines. 
+
+  @{ML_response [display, gray]
+  "cat_lines [\"foo\", \"bar\"]"
+  "\"foo\\nbar\""}
+*}
+
+
 section {* Combinators\label{sec:combinators} *}
 
 text {*
@@ -746,9 +758,9 @@
   val v2 = Var ((\"x1\", 3), @{typ bool})
   val v3 = Free (\"x\", @{typ bool})
 in
-  tracing (Syntax.string_of_term @{context} v1);
-  tracing (Syntax.string_of_term @{context} v2);
-  tracing (Syntax.string_of_term @{context} v3)
+  map (Syntax.string_of_term @{context}) [v1, v2, v3]
+  |> cat_lines
+  |> tracing
 end"
 "?x3
 ?x1.3