--- a/ProgTutorial/General.thy	Tue Nov 17 23:59:19 2009 +0100
+++ b/ProgTutorial/General.thy	Wed Nov 18 14:06:01 2009 +0100
@@ -185,29 +185,27 @@
   "@{typ \"bool\"}"
   "bool"}
 
-  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 (it 
-  uses pretty-printing functions which will be explained in more detail in 
-  Section~\ref{sec:pretty}).
+  that is the pretty printed version of @{text "bool"}. However, in PolyML
+  (version 5.3) it is easy to install your own pretty printer. With the
+  function below we 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 raw_pp_typ ty =
-let
-  fun pp_pair (x1, x2) = Pretty.list "(" ")" [x1, x2]
+ML{*local
+  fun pp_pair (x, y) = Pretty.list "(" ")" [x, y]
   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]
+  fun pp_constr a args = Pretty.block [pp_str a, Pretty.brk 1, args]
 in
-  case ty of
-    TVar ((a, i), S) => 
+fun raw_pp_typ (TVar ((a, i), S)) = 
       pp_constr "TVar" (pp_pair (pp_pair (pp_qstr a, pp_int i), pp_sort S))
-  | TFree (a, S) => 
+  | raw_pp_typ (TFree (a, S)) = 
       pp_constr "TFree" (pp_pair (pp_qstr a, pp_sort S))
-  | Type (a, tys) => 
+  | raw_pp_typ (Type (a, tys)) = 
       pp_constr "Type" (pp_pair (pp_qstr a, pp_list (map raw_pp_typ tys)))
 end*}
 
@@ -216,11 +214,8 @@
   @{ML_ind addPrettyPrinter in PolyML} as follows.
 *}
 
-ML{*let
-  fun pp _ _ = ml_pretty o Pretty.to_ML o raw_pp_typ
-in
-  PolyML.addPrettyPrinter pp
-end*}
+ML{*PolyML.addPrettyPrinter 
+  (fn _ => fn _ => ml_pretty o Pretty.to_ML o raw_pp_typ)*}
 
 text {*
   Now the type bool is printed out in full detail.
@@ -250,11 +245,8 @@
   with the code
 *}
 
-ML{*let
-  fun pp _ _ = ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy
-in
-  PolyML.addPrettyPrinter pp
-end*}
+ML{*PolyML.addPrettyPrinter 
+  (fn _ => fn _ => ml_pretty o Pretty.to_ML o Proof_Display.pp_typ Pure.thy)*}
 
 text {*
   After that the types for booleans, lists and so on are printed out again 

Binary file progtutorial.pdf has changed