1.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Mon Sep 12 10:49:37 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Mon Sep 12 10:49:37 2011 +0200
     1.3 @@ -123,7 +123,9 @@
     1.4    Sign.typ_instance (Proof_Context.theory_of ctxt) (T, T')
     1.5  fun type_generalization ctxt T T' = type_instance ctxt T' T
     1.6  fun type_intersect ctxt T T' =
     1.7 -  can (Sign.typ_unify (Proof_Context.theory_of ctxt) (T, T')) (Vartab.empty, 0)
     1.8 +  can (Sign.typ_unify (Proof_Context.theory_of ctxt)
     1.9 +                      (T, Logic.incr_tvar (maxidx_of_typ T + 1) T'))
    1.10 +      (Vartab.empty, 0)
    1.11  val type_equiv = Sign.typ_equiv o Proof_Context.theory_of
    1.12  
    1.13  fun varify_type ctxt T =