equal
deleted
inserted
replaced
211 val declare_type_occs = map_type_occs o decl_type_occs; |
211 val declare_type_occs = map_type_occs o decl_type_occs; |
212 |
212 |
213 |
213 |
214 (* constraints *) |
214 (* constraints *) |
215 |
215 |
216 fun constrain_tvar (xi, S) = |
216 fun constrain_tvar (xi, raw_S) = |
217 if S = dummyS orelse Term_Position.is_positionS S |
217 let val (_, S) = Term_Position.decode_positionS raw_S |
218 then Vartab.delete_safe xi else Vartab.update (xi, S); |
218 in if S = dummyS then Vartab.delete_safe xi else Vartab.update (xi, S) end; |
219 |
219 |
220 fun declare_constraints t = map_constraints (fn (types, sorts) => |
220 fun declare_constraints t = map_constraints (fn (types, sorts) => |
221 let |
221 let |
222 val types' = fold_aterms |
222 val types' = fold_aterms |
223 (fn Free (x, T) => Vartab.update ((x, ~1), T) |
223 (fn Free (x, T) => Vartab.update ((x, ~1), T) |