128 |
128 |
129 val string_from_time = string_from_ext_time o pair false |
129 val string_from_time = string_from_ext_time o pair false |
130 |
130 |
131 fun type_instance thy T T' = Sign.typ_instance thy (T, T') |
131 fun type_instance thy T T' = Sign.typ_instance thy (T, T') |
132 fun type_generalization thy T T' = Sign.typ_instance thy (T', T) |
132 fun type_generalization thy T T' = Sign.typ_instance thy (T', T) |
133 fun type_intersect thy T T' = |
133 |
134 can (Sign.typ_unify thy (Logic.incr_tvar (maxidx_of_typ T' + 1) T, T')) |
134 fun type_intersect _ (TVar _) _ = true |
135 (Vartab.empty, 0) |
135 | type_intersect _ _ (TVar _) = true |
|
136 | type_intersect thy T T' = |
|
137 let |
|
138 val tvars = Term.add_tvar_namesT T [] |
|
139 val tvars' = Term.add_tvar_namesT T' [] |
|
140 val T = |
|
141 if exists (member (op =) tvars') tvars then |
|
142 T |> Logic.incr_tvar (maxidx_of_typ T' + 1) |
|
143 else |
|
144 T |
|
145 in can (Sign.typ_unify thy (T, T')) (Vartab.empty, 0) end |
|
146 |
136 val type_equiv = Sign.typ_equiv |
147 val type_equiv = Sign.typ_equiv |
137 |
148 |
138 fun varify_type ctxt T = |
149 fun varify_type ctxt T = |
139 Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)] |
150 Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)] |
140 |> snd |> the_single |> dest_Const |> snd |
151 |> snd |> the_single |> dest_Const |> snd |