--- a/ProgTutorial/Tactical.thy	Wed Mar 25 15:09:04 2009 +0100
+++ b/ProgTutorial/Tactical.thy	Thu Mar 26 19:00:51 2009 +0000
@@ -1148,17 +1148,13 @@
   fun name_ctrm (nm, ctrm) =
       "  " ^ nm ^ ": " ^ (str_of_cterms ctxt ctrm)
 
-  val s1 = ["Simplification rules:"]
-  val s2 = map name_thm simps
-  val s3 = ["Congruences rules:"]
-  val s4 = map name_thm congs
-  val s5 = ["Simproc patterns:"]
-  val s6 = map name_ctrm procs
+  val s = ["Simplification rules:"] @ (map name_thm simps) @
+          ["Congruences rules:"] @ (map name_thm congs) @
+          ["Simproc patterns:"] @ (map name_ctrm procs)
 in
-  (s1 @ s2 @ s3 @ s4 @ s5 @ s6) 
-     |> separate "\n"
-     |> implode
-     |> warning
+  s |> separate "\n"
+    |> implode
+    |> warning
 end*}
 text_raw {* 
 \end{isabelle}