# 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])