1.1 --- a/src/Pure/General/pretty.ML	Tue Aug 17 23:23:29 2010 +0200
     1.2 +++ b/src/Pure/General/pretty.ML	Wed Aug 18 11:02:47 2010 +0200
     1.3 @@ -132,7 +132,7 @@
     1.4  
     1.5  fun markup_block m arg = block_markup (Markup.output m) arg;
     1.6  
     1.7 -val blk = markup_block Markup.none;
     1.8 +val blk = markup_block Markup.empty;
     1.9  fun block prts = blk (2, prts);
    1.10  val strs = block o breaks o map str;
    1.11  
    1.12 @@ -142,7 +142,7 @@
    1.13  fun command name = mark Markup.command (str name);
    1.14  
    1.15  fun markup_chunks m prts = markup m (fbreaks prts);
    1.16 -val chunks = markup_chunks Markup.none;
    1.17 +val chunks = markup_chunks Markup.empty;
    1.18  fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts)));
    1.19  
    1.20  fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];