diff -r 2f39df9ceb63 -r 4c32349b9875 ProgTutorial/First_Steps.thy --- 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}