# HG changeset patch
# User paulson
# Date 846859177 -3600
# Node ID 639db817780404e767f478ef414a546591784877
# Parent  7ef2987da18f3a2231dee7c7a7f74029e304182d
Now uses Int.max instead of max

diff -r 7ef2987da18f -r 639db8177804 src/Pure/Syntax/pretty.ML
--- a/src/Pure/Syntax/pretty.ML	Fri Nov 01 15:37:30 1996 +0100
+++ b/src/Pure/Syntax/pretty.ML	Fri Nov 01 15:39:37 1996 +0100
@@ -125,8 +125,8 @@
                             or if breaking would add only breakgain to space *)
            format (es,blockin,after)
                (if not force andalso
-                   pos+wd <= max[!margin - breakdist(es,after),
-                                 blockin + !breakgain]
+                   pos+wd <= Int.max(!margin - breakdist(es,after),
+				     blockin + !breakgain)
                 then blanks wd text  (*just insert wd blanks*)
                 else blanks blockin (newline text)));