1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jul 11 21:43:19 2012 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Wed Jul 11 21:43:19 2012 +0200
     1.3 @@ -419,7 +419,7 @@
     1.4  fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
     1.5  
     1.6  val tvar_a_str = "'a"
     1.7 -val tvar_a_z = ((tvar_a_str, 0), HOLogic.typeS)
     1.8 +val tvar_a_z = ((tvar_a_str, 100 (* arbitrary *)), HOLogic.typeS)
     1.9  val tvar_a = TVar tvar_a_z
    1.10  val tvar_a_name = tvar_name tvar_a_z
    1.11  val itself_name = `make_fixed_type_const @{type_name itself}

     2.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Wed Jul 11 21:43:19 2012 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Wed Jul 11 21:43:19 2012 +0200
     2.3 @@ -130,9 +130,20 @@
     2.4  
     2.5  fun type_instance thy T T' = Sign.typ_instance thy (T, T')
     2.6  fun type_generalization thy T T' = Sign.typ_instance thy (T', T)
     2.7 -fun type_intersect thy T T' =
     2.8 -  can (Sign.typ_unify thy (Logic.incr_tvar (maxidx_of_typ T' + 1) T, T'))
     2.9 -      (Vartab.empty, 0)
    2.10 +
    2.11 +fun type_intersect _ (TVar _) _ = true
    2.12 +  | type_intersect _ _ (TVar _) = true
    2.13 +  | type_intersect thy T T' =
    2.14 +    let
    2.15 +      val tvars = Term.add_tvar_namesT T []
    2.16 +      val tvars' = Term.add_tvar_namesT T' []
    2.17 +      val T =
    2.18 +        if exists (member (op =) tvars') tvars then
    2.19 +          T |> Logic.incr_tvar (maxidx_of_typ T' + 1)
    2.20 +        else
    2.21 +          T
    2.22 +    in can (Sign.typ_unify thy (T, T')) (Vartab.empty, 0) end
    2.23 +
    2.24  val type_equiv = Sign.typ_equiv
    2.25  
    2.26  fun varify_type ctxt T =