omit redundant combinators (amending 7456a64bc4f6);
authorwenzelm
Thu, 28 Nov 2024 19:35:30 +0100
changeset 81504 7b85ebdab12c
parent 81503 60e61a934a80
child 81505 01f2936ec85e
omit redundant combinators (amending 7456a64bc4f6);
src/Pure/variable.ML
--- a/src/Pure/variable.ML	Thu Nov 28 14:12:13 2024 +0100
+++ b/src/Pure/variable.ML	Thu Nov 28 19:35:30 2024 +0100
@@ -214,12 +214,12 @@
 (* names *)
 
 fun declare_type_names t =
-  map_names (fold_types (fold_atyps Term.declare_typ_names) t) #>
+  map_names (fold_types Term.declare_typ_names t) #>
   map_maxidx (fold_types Term.maxidx_typ t);
 
 fun declare_names t =
   declare_type_names t #>
-  map_names (fold_aterms Term.declare_term_frees t) #>
+  map_names (Term.declare_term_frees t) #>
   map_maxidx (Term.maxidx_term t);