src/HOL/Tools/ATP/atp_util.ML
changeset 44893 bdc64c34ccae
parent 44859 237ba63d6041
child 44935 2e812384afa8
--- 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 =