Now uses Int.max instead of max

--- 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)));