equal
deleted
inserted
replaced
212 |
212 |
213 |
213 |
214 (* names *) |
214 (* names *) |
215 |
215 |
216 fun declare_type_names t = |
216 fun declare_type_names t = |
217 map_names (fold_types Term.declare_typ_names t) #> |
217 map_names (Term.declare_tfree_names t) #> |
218 map_maxidx (fold_types Term.maxidx_typ t); |
218 map_maxidx (fold_types Term.maxidx_typ t); |
219 |
219 |
220 fun declare_names t = |
220 fun declare_names t = |
221 declare_type_names t #> |
221 declare_type_names t #> |
222 map_names (Term.declare_term_frees t) #> |
222 map_names (Term.declare_free_names t) #> |
223 map_maxidx (Term.maxidx_term t); |
223 map_maxidx (Term.maxidx_term t); |
224 |
224 |
225 |
225 |
226 (* type occurrences *) |
226 (* type occurrences *) |
227 |
227 |