--- a/ProgTutorial/First_Steps.thy	Fri Aug 13 18:05:30 2010 +0800
+++ b/ProgTutorial/First_Steps.thy	Fri Aug 13 18:42:58 2010 +0800
@@ -250,11 +250,12 @@
   "\"1\""}
 
   If there is more than one term to be printed, you can use the 
-  function @{ML_ind enum in Pretty} and commas to separate them.
+  function @{ML_ind commas in Pretty} and @{ML_ind block in Pretty} 
+  to separate them.
 *} 
 
 ML{*fun pretty_terms ctxt ts =  
-  Pretty.enum "," "" "" (map (pretty_term ctxt) ts)*}
+  Pretty.block (Pretty.commas (map (pretty_term ctxt) ts))*}
 
 text {*
   You can also print out terms together with their typing information.
@@ -299,11 +300,11 @@
 text {*
   Here the function @{ML_ind term_of in Thm} extracts the @{ML_type
   term} from a @{ML_type cterm}.  More than one @{ML_type cterm}s can be
-  printed again with @{ML enum in Pretty}.
+  printed again with @{ML commas in Pretty}.
 *} 
 
 ML{*fun pretty_cterms ctxt cts =  
-  Pretty.enum "," "" "" (map (pretty_cterm ctxt) cts)*}
+  Pretty.block (Pretty.commas (map (pretty_cterm ctxt) cts))*}
 
 text {*
   The easiest way to get the string of a theorem is to transform it
@@ -352,24 +353,26 @@
 *}
 
 ML{*fun pretty_thms ctxt thms =  
-  Pretty.enum "," "" "" (map (pretty_thm ctxt) thms)
+  Pretty.block (Pretty.commas (map (pretty_thm ctxt) thms))
 
 fun pretty_thms_no_vars ctxt thms =  
-  Pretty.enum "," "" "" (map (pretty_thm_no_vars ctxt) thms)*}
+  Pretty.block (Pretty.commas (map (pretty_thm_no_vars ctxt) thms))*}
 
 text {*
   The printing functions for types are
 *}
 
 ML{*fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty
-fun pretty_typs ctxt tys = Pretty.commas (map (pretty_typ ctxt) tys)*}
+fun pretty_typs ctxt tys = 
+  Pretty.block (Pretty.commas (map (pretty_typ ctxt) tys))*}
 
 text {*
   respectively ctypes
 *}
 
 ML{*fun pretty_ctyp ctxt cty = pretty_typ ctxt (typ_of cty)
-fun pretty_ctyps ctxt ctys = Pretty.commas (map (pretty_ctyp ctxt) ctys)*}
+fun pretty_ctyps ctxt ctys = 
+  Pretty.block (Pretty.commas (map (pretty_ctyp ctxt) ctys))*}
 
 text {*
   \begin{readmore}