fbrk: 2 if not taken;
authorwenzelm
Sun Jun 25 23:46:22 2000 +0200 (2000-06-25)
changeset 912125245986e667
parent 9120 04a46ceace35
child 9122 addbea344673
fbrk: 2 if not taken;
src/Pure/General/pretty.ML
     1.1 --- a/src/Pure/General/pretty.ML	Sun Jun 25 23:46:03 2000 +0200
     1.2 +++ b/src/Pure/General/pretty.ML	Sun Jun 25 23:46:22 2000 +0200
     1.3 @@ -147,7 +147,7 @@
     1.4  val str = String o apsnd Real.round o Symbol.output_width;
     1.5  
     1.6  fun brk wd = Break (false, wd);
     1.7 -val fbrk = Break (true, 0);
     1.8 +val fbrk = Break (true, 2);
     1.9  
    1.10  fun blk (indent, es) =
    1.11    let