src/HOL/Tools/ATP/atp_util.ML
changeset 44893 bdc64c34ccae
parent 44859 237ba63d6041
child 44935 2e812384afa8
equal deleted inserted replaced
44892:a41eacd1ae8d 44893:bdc64c34ccae
   121 
   121 
   122 fun type_instance ctxt T T' =
   122 fun type_instance ctxt T T' =
   123   Sign.typ_instance (Proof_Context.theory_of ctxt) (T, T')
   123   Sign.typ_instance (Proof_Context.theory_of ctxt) (T, T')
   124 fun type_generalization ctxt T T' = type_instance ctxt T' T
   124 fun type_generalization ctxt T T' = type_instance ctxt T' T
   125 fun type_intersect ctxt T T' =
   125 fun type_intersect ctxt T T' =
   126   can (Sign.typ_unify (Proof_Context.theory_of ctxt) (T, T')) (Vartab.empty, 0)
   126   can (Sign.typ_unify (Proof_Context.theory_of ctxt)
       
   127                       (T, Logic.incr_tvar (maxidx_of_typ T + 1) T'))
       
   128       (Vartab.empty, 0)
   127 val type_equiv = Sign.typ_equiv o Proof_Context.theory_of
   129 val type_equiv = Sign.typ_equiv o Proof_Context.theory_of
   128 
   130 
   129 fun varify_type ctxt T =
   131 fun varify_type ctxt T =
   130   Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
   132   Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
   131   |> snd |> the_single |> dest_Const |> snd
   133   |> snd |> the_single |> dest_Const |> snd