optimized type intersection, hoping this will reduce the number of sudden Interrupts in the "incr_tvar" code
--- a/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jul 11 21:43:19 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_problem_generate.ML Wed Jul 11 21:43:19 2012 +0200
@@ -419,7 +419,7 @@
fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
val tvar_a_str = "'a"
-val tvar_a_z = ((tvar_a_str, 0), HOLogic.typeS)
+val tvar_a_z = ((tvar_a_str, 100 (* arbitrary *)), HOLogic.typeS)
val tvar_a = TVar tvar_a_z
val tvar_a_name = tvar_name tvar_a_z
val itself_name = `make_fixed_type_const @{type_name itself}
--- a/src/HOL/Tools/ATP/atp_util.ML Wed Jul 11 21:43:19 2012 +0200
+++ b/src/HOL/Tools/ATP/atp_util.ML Wed Jul 11 21:43:19 2012 +0200
@@ -130,9 +130,20 @@
fun type_instance thy T T' = Sign.typ_instance thy (T, T')
fun type_generalization thy T T' = Sign.typ_instance thy (T', T)
-fun type_intersect thy T T' =
- can (Sign.typ_unify thy (Logic.incr_tvar (maxidx_of_typ T' + 1) T, T'))
- (Vartab.empty, 0)
+
+fun type_intersect _ (TVar _) _ = true
+ | type_intersect _ _ (TVar _) = true
+ | type_intersect thy T T' =
+ let
+ val tvars = Term.add_tvar_namesT T []
+ val tvars' = Term.add_tvar_namesT T' []
+ val T =
+ if exists (member (op =) tvars') tvars then
+ T |> Logic.incr_tvar (maxidx_of_typ T' + 1)
+ else
+ T
+ in can (Sign.typ_unify thy (T, T')) (Vartab.empty, 0) end
+
val type_equiv = Sign.typ_equiv
fun varify_type ctxt T =