# HG changeset patch
# User haftmann
# Date 1127291978 -7200
# Node ID b588e06b6775506bf56666a66e4a6d162fc7d473
# Parent  6a52083b71c331ee7c5277fda10d0bc5900c17c1
(name mess cleanup)

diff -r 6a52083b71c3 -r b588e06b6775 src/Pure/General/pretty.ML
--- 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));