--- a/ProgTutorial/Tactical.thy	Mon Jul 19 15:44:13 2010 +0100
+++ b/ProgTutorial/Tactical.thy	Tue Jul 20 13:34:44 2010 +0100
@@ -252,7 +252,7 @@
 
 ML{*fun my_print_tac ctxt thm =
 let
-  val _ = tracing (string_of_thm_no_vars ctxt thm)
+  val _ = tracing (Pretty.string_of (pretty_thm_no_vars ctxt thm))
 in 
   Seq.single thm
 end*}
@@ -544,24 +544,19 @@
 
 ML{*fun foc_tac {prems, params, asms, concl, context, schematics} = 
 let 
-  fun pairs1 f1 f2 xs =
-    commas (map (fn (x, y) => f1 x ^ ":=" ^ f2 y) xs) 
-
-  fun pairs2 f xs = pairs1 f f xs 
-
-  val string_of_params = pairs1 I (string_of_cterm context) params
-  val string_of_asms = string_of_cterms context asms
-  val string_of_concl = string_of_cterm context concl
-  val string_of_prems = string_of_thms_no_vars context prems   
-  val string_of_schms = pairs2 (string_of_cterm context) (snd schematics)
-
-  val strs = ["params: " ^ string_of_params,
-              "schematics: " ^ string_of_schms,
-              "assumptions: " ^ string_of_asms,
-              "conclusion: " ^ string_of_concl,
-              "premises: " ^ string_of_prems]
+  fun assgn1 f1 f2 xs =
+    Pretty.list "" "" (map (fn (x, y) => Pretty.enum ":=" "" "" [f1 x, f2 y]) xs) 
+
+  fun assgn2 f xs = assgn1 f f xs 
+ 
+  val pps = map (fn (s, pp) => Pretty.block [Pretty.str s, pp])
+    [("params: ", assgn1 Pretty.str (pretty_cterm context) params),
+     ("assumptions: ", pretty_cterms context asms),
+     ("conclusion: ", pretty_cterm context concl),
+     ("premises: ", pretty_thms_no_vars context prems),   
+     ("schematics: ", assgn2 (pretty_cterm context) (snd schematics))]
 in
-  tracing (cat_lines strs); all_tac 
+  tracing (Pretty.string_of (Pretty.chunks pps)); all_tac 
 end*}
 
 text_raw{*
@@ -583,7 +578,7 @@
 
   \begin{quote}\small
   \begin{tabular}{ll}
-  params:      & @{text "x:=x"}, @{text "y:=y"}\\
+  params:      & @{text "x:= x"}, @{text "y:= y"}\\
   schematics:  & @{text "?z:=z"}\\
   assumptions: & @{term "A x y"}\\
   conclusion:  & @{term "B y x \<longrightarrow> C (z y) x"}\\
@@ -611,7 +606,7 @@
 
   \begin{quote}\small
   \begin{tabular}{ll}
-  params:      & @{text "x:=x"}, @{text "y:=y"}\\
+  params:      & @{text "x:= x"}, @{text "y:= y"}\\
   schematics:  & @{text "?z:=z"}\\
   assumptions: & @{term "A x y"}, @{term "B y x"}\\
   conclusion:  & @{term "C (z y) x"}\\
@@ -1493,16 +1488,16 @@
   val {simps, congs, procs, ...} = MetaSimplifier.dest_ss ss
 
   fun name_thm (nm, thm) =
-      "  " ^ nm ^ ": " ^ (string_of_thm_no_vars ctxt thm)
+    Pretty.enclose (nm ^ ": ") "" [pretty_thm_no_vars ctxt thm]
   fun name_ctrm (nm, ctrm) =
-      "  " ^ nm ^ ": " ^ (string_of_cterms ctxt ctrm)
-
-  val s = ["Simplification rules:"] @ map name_thm simps @
-          ["Congruences rules:"] @ map name_thm congs @
-          ["Simproc patterns:"] @ map name_ctrm procs
+    Pretty.enclose (nm ^ ": ") "" [pretty_cterms ctxt ctrm]
+
+  val pps = [Pretty.big_list "Simplification rules:" (map name_thm simps),
+             Pretty.big_list "Congruences rules:" (map name_thm congs),
+             Pretty.big_list "Simproc patterns:" (map name_ctrm procs)]
 in
-  s |> cat_lines
-    |> tracing
+  pps |> Pretty.chunks
+      |> pwriteln
 end*}
 text_raw {* 
 \end{isabelle}