# HG changeset patch
# User paulson
# Date 846859550 -3600
# Node ID 76d5ed939545dfad2d90ac73603eaf99649a1148
# Parent  0007679951438fe7a478905e55a4006af7962505
Now uses Int.max instead of max

diff -r 000767995143 -r 76d5ed939545 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Fri Nov 01 15:42:40 1996 +0100
+++ b/src/Pure/drule.ML	Fri Nov 01 15:45:50 1996 +0100
@@ -432,9 +432,9 @@
   Instantiates distinct Vars by terms, inferring type instantiations. *)
 local
   fun add_types ((ct,cu), (sign,tye,maxidx)) =
-    let val {sign=signt, t=t, T= T, maxidx=maxidxt,...} = rep_cterm ct
-        and {sign=signu, t=u, T= U, maxidx=maxidxu,...} = rep_cterm cu;
-        val maxi = max[maxidx,maxidxt,maxidxu];
+    let val {sign=signt, t=t, T= T, maxidx=maxt,...} = rep_cterm ct
+        and {sign=signu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu;
+        val maxi = Int.max(maxidx, Int.max(maxt, maxu));
         val sign' = Sign.merge(sign, Sign.merge(signt, signu))
         val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) maxi tye (T,U)
           handle Type.TUNIFY => raise TYPE("add_types", [T,U], [t,u])