--- a/src/Pure/General/pretty.ML Wed Sep 21 10:33:59 2005 +0200
+++ b/src/Pure/General/pretty.ML Wed Sep 21 10:39:38 2005 +0200
@@ -205,10 +205,10 @@
fun quote prt =
blk (1, [str "\"", prt, str "\""]);
-fun separate_pretty delim prts =
+fun separate_pretty sep prts =
prts
|> map single
- |> separate [str delim, brk 1]
+ |> separate [str sep, brk 1]
|> List.concat;
val commas = separate_pretty ",";
@@ -223,7 +223,7 @@
fun enclose lpar rpar prts =
block (str lpar :: (prts @ [str rpar]));
-fun gen_list delim lpar rpar prts = enclose lpar rpar (separate_pretty delim prts);
+fun gen_list sep lpar rpar prts = enclose lpar rpar (separate_pretty sep prts);
val list = gen_list ",";
fun str_list lpar rpar strs = list lpar rpar (map str strs);
fun big_list name prts = block (fbreaks (str name :: prts));