# HG changeset patch
# User wenzelm
# Date 1732818930 -3600
# Node ID 7b85ebdab12cfae408991b55a2e010b9c89a0fdc
# Parent  60e61a934a80cc7db2c201f6d835f14ba608ccaa
omit redundant combinators (amending 7456a64bc4f6);

diff -r 60e61a934a80 -r 7b85ebdab12c 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);