diff -r b1956bc8f585 -r 58020b59baf7 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Thu May 06 22:54:25 2010 +0200
+++ b/src/Pure/General/pretty.ML	Thu May 06 23:07:21 2010 +0200
@@ -249,9 +249,9 @@
 
 (*Add the lengths of the expressions until the next Break; if no Break then
   include "after", to account for text following this block.*)
-fun breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after)
+fun breakdist (Break _ :: _, _) = 0
+  | breakdist (Block (_, _, _, len) :: es, after) = len + breakdist (es, after)
   | breakdist (String (_, len) :: es, after) = len + breakdist (es, after)
-  | breakdist (Break _ :: _, _) = 0
   | breakdist ([], after) = after;
 
 (*Search for the next break (at this or higher levels) and force it to occur.*)
@@ -280,7 +280,6 @@
             (*if this block was broken then force the next break*)
             val es' = if nl < #nl btext then forcenext es else es;
           in format (es', block, after) btext end
-      | String str => format (es, block, after) (string str text)
       | Break (force, wd) =>
           let val {margin, breakgain, ...} = ! margin_info in
             (*no break if text to next break fits on this line
@@ -290,7 +289,8 @@
                   pos + wd <= Int.max (margin - breakdist (es, after), blockin + breakgain)
                 then text |> blanks wd  (*just insert wd blanks*)
                 else text |> newline |> indentation block)
-          end);
+          end
+      | String str => format (es, block, after) (string str text));
 
 in