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