src/Pure/drule.ML
changeset 12527 d6c91bc3e49c
parent 12495 89f97fa683f5
child 12710 d9e0674653b3
     1.1 --- a/src/Pure/drule.ML	Mon Dec 17 14:27:18 2001 +0100
     1.2 +++ b/src/Pure/drule.ML	Tue Dec 18 02:17:20 2001 +0100
     1.3 @@ -706,7 +706,7 @@
     1.4          and {sign=signu, t=u, T= U, maxidx=maxu,...} = rep_cterm cu;
     1.5          val maxi = Int.max(maxidx, Int.max(maxt, maxu));
     1.6          val sign' = Sign.merge(sign, Sign.merge(signt, signu))
     1.7 -        val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) maxi tye (T,U)
     1.8 +        val (tye',maxi') = Type.unify (#tsig(Sign.rep_sg sign')) (tye, maxi) (T, U)
     1.9            handle Type.TUNIFY => raise TYPE("Ill-typed instantiation", [T,U], [t,u])
    1.10      in  (sign', tye', maxi')  end;
    1.11  in