# HG changeset patch
# User blanchet
# Date 1315817377 -7200
# Node ID bdc64c34ccae42ae9b982ef2915b0d8a94848ba2
# Parent  a41eacd1ae8db7ff24c9ac433bd6243d425fbc67
fixed type intersection (again)

diff -r a41eacd1ae8d -r bdc64c34ccae src/HOL/Tools/ATP/atp_util.ML
--- 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 =