1.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Fri Jan 18 00:18:11 2013 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Fri Jan 18 14:33:16 2013 +0100
     1.3 @@ -156,12 +156,11 @@
     1.4      let
     1.5        val tvars = Term.add_tvar_namesT T []
     1.6        val tvars' = Term.add_tvar_namesT T' []
     1.7 +      val maxidx' = maxidx_of_typ T'
     1.8        val T =
     1.9 -        if exists (member (op =) tvars') tvars then
    1.10 -          T |> Logic.incr_tvar (maxidx_of_typ T' + 1)
    1.11 -        else
    1.12 -          T
    1.13 -    in can (Sign.typ_unify thy (T, T')) (Vartab.empty, 0) end
    1.14 +        T |> exists (member (op =) tvars') tvars ? Logic.incr_tvar (maxidx' + 1)
    1.15 +      val maxidx = Integer.max (maxidx_of_typ T) maxidx'
    1.16 +    in can (Sign.typ_unify thy (T, T')) (Vartab.empty, maxidx) end
    1.17  
    1.18  val type_equiv = Sign.typ_equiv
    1.19