| changeset 81505 | 01f2936ec85e |
| parent 81504 | 7b85ebdab12c |
| child 81512 | c1aa8a61ee65 |
--- a/src/Pure/variable.ML Thu Nov 28 19:35:30 2024 +0100 +++ b/src/Pure/variable.ML Fri Nov 29 00:25:03 2024 +0100 @@ -214,12 +214,12 @@ (* names *) fun declare_type_names t = - map_names (fold_types Term.declare_typ_names t) #> + map_names (Term.declare_tfree_names t) #> map_maxidx (fold_types Term.maxidx_typ t); fun declare_names t = declare_type_names t #> - map_names (Term.declare_term_frees t) #> + map_names (Term.declare_free_names t) #> map_maxidx (Term.maxidx_term t);