back to 1.36 (Poly/ML crash!?);
authorwenzelm
Tue, 24 Jun 2008 23:38:44 +0200
changeset 27350c8adf88960ad
parent 27349 80273a002e37
child 27351 6b120fb45278
back to 1.36 (Poly/ML crash!?);
src/Pure/General/pretty.ML
     1.1 --- a/src/Pure/General/pretty.ML	Tue Jun 24 22:27:36 2008 +0200
     1.2 +++ b/src/Pure/General/pretty.ML	Tue Jun 24 23:38:44 2008 +0200
     1.3 @@ -322,9 +322,7 @@
     1.4  (*ML toplevel pretty printing*)
     1.5  fun pprint prt (put_str, begin_blk, put_brk, put_fbrk, end_blk) =
     1.6    let
     1.7 -    fun pp (Block (m, prts, ind, _)) =
     1.8 -          let val (bg, en) = Markup.output m
     1.9 -          in put_str bg; begin_blk ind; pp_lst prts; end_blk (); put_str en end
    1.10 +    fun pp (Block (_, prts, ind, _)) = (begin_blk ind; pp_lst prts; end_blk ())
    1.11        | pp (String (s, _)) = put_str s
    1.12        | pp (Break (false, wd)) = put_brk wd
    1.13        | pp (Break (true, _)) = put_fbrk ()