# HG changeset patch
# User blanchet
# Date 1342035799 -7200
# Node ID 8f37d2ddabc8a7db82f5289aa13ccca757378973
# Parent  fb11c09d7729a52ea1ca8265bf339770a1c232ce
optimized type intersection, hoping this will reduce the number of sudden Interrupts in the "incr_tvar" code

diff -r fb11c09d7729 -r 8f37d2ddabc8 src/HOL/Tools/ATP/atp_problem_generate.ML
--- 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}
diff -r fb11c09d7729 -r 8f37d2ddabc8 src/HOL/Tools/ATP/atp_util.ML
--- 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 =