--- a/ProgTutorial/General.thy	Tue Nov 17 20:36:18 2009 +0100
+++ b/ProgTutorial/General.thy	Tue Nov 17 23:59:19 2009 +0100
@@ -187,23 +187,28 @@
 
   that is the pretty printed version of @{text "bool"}. However, in PolyML it is 
   easy to install your own pretty printer. With the function below we 
-  mimic the behaviour of the usual pretty printer for 
-  datatypes.\footnote{Thanks to David Matthews for providing this
-  code.}
+  mimic the behaviour of the usual pretty printer for datatypes (it 
+  uses pretty-printing functions which will be explained in more detail in 
+  Section~\ref{sec:pretty}).
 *}
 
-ML{*fun typ_raw_pretty_printer depth _ ty =
+ML{*fun raw_pp_typ ty =
 let
- fun cond str a =
-   if depth <= 0 
-   then PolyML.PrettyString "..."
-   else PolyML.PrettyBlock(1, false, [], 
-          [PolyML.PrettyString str, PolyML.PrettyBreak(1, 0), a])
-in 
+  fun pp_pair (x1, x2) = Pretty.list "(" ")" [x1, x2]
+  fun pp_list xs = Pretty.list "[" "]" xs
+  fun pp_str s   = Pretty.str s
+  fun pp_qstr s  = Pretty.quote (pp_str s)
+  fun pp_int i   = pp_str (string_of_int i)
+  fun pp_sort S  = pp_list (map pp_qstr S)
+  fun pp_constr s xs = Pretty.block [pp_str s, Pretty.brk 1, xs]
+in
   case ty of
-    Type a  => cond "Type"  (PolyML.prettyRepresentation(a, depth - 1))
-  | TFree a => cond "TFree" (PolyML.prettyRepresentation(a, depth - 1)) 
-  | TVar a  => cond "TVar"  (PolyML.prettyRepresentation(a, depth - 1))
+    TVar ((a, i), S) => 
+      pp_constr "TVar" (pp_pair (pp_pair (pp_qstr a, pp_int i), pp_sort S))
+  | TFree (a, S) => 
+      pp_constr "TFree" (pp_pair (pp_qstr a, pp_sort S))
+  | Type (a, tys) => 
+      pp_constr "Type" (pp_pair (pp_qstr a, pp_list (map raw_pp_typ tys)))
 end*}
 
 text {*
@@ -211,23 +216,11 @@
   @{ML_ind addPrettyPrinter in PolyML} as follows.
 *}
 
-ML{*PolyML.addPrettyPrinter typ_raw_pretty_printer*}
-
-(*
-classes s
-
-ML {* @{typ "bool \<Rightarrow> ('a::s)"} *}
-
-ML {* 
-fun test ty =
-  case ty of
-    TVar ((v, n), s) => Pretty.block [Pretty.str "TVar "]
-  | TFree (x, s) => Pretty.block [Pretty.str "TFree "]
-  | Type (s, tys) => Pretty.block [Pretty.str "Type "]
-*}
-
-ML {* toplevel_pp ["typ"] "test" *}
-*)
+ML{*let
+  fun pp _ _ = ml_pretty o Pretty.to_ML o raw_pp_typ
+in
+  PolyML.addPrettyPrinter pp
+end*}
 
 text {*
   Now the type bool is printed out in full detail.
@@ -257,10 +250,11 @@
   with the code
 *}
 
-ML{*fun stnd_pretty_printer _ _ =   
-  ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy;
-
-PolyML.addPrettyPrinter stnd_pretty_printer*}
+ML{*let
+  fun pp _ _ = ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy
+in
+  PolyML.addPrettyPrinter pp
+end*}
 
 text {*
   After that the types for booleans, lists and so on are printed out again 
@@ -2089,6 +2083,9 @@
   valid local theory.
 
   @{ML "Context.>> o Context.map_theory"}
+
+  \footnote{\bf FIXME: list append in merge operations can cause 
+  exponential blowups.}
 *}
 
 section {* Setups (TBD) *}