diff -r b43192613888 -r bbed9f218158 src/Pure/more_pattern.ML
--- a/src/Pure/more_pattern.ML	Thu Oct 24 12:44:48 2024 +0200
+++ b/src/Pure/more_pattern.ML	Thu Oct 24 22:05:57 2024 +0200
@@ -14,7 +14,7 @@
   val first_order: term -> bool
   val match_rew: theory -> term -> term * term -> (term * term) option
   val rewrite_term: theory -> (term * term) list -> (term -> term option) list -> term -> term
-  val rewrite_term_top: theory -> (term * term) list -> (term -> term option) list -> term -> term
+  val rewrite_term_topdown: theory -> (term * term) list -> (term -> term option) list -> term -> term
   val rewrite_term_yoyo: theory -> (term * term) list -> (term -> term option) list -> term -> term
 end;
 
@@ -137,7 +137,7 @@
 in
 
 val rewrite_term = rewrite_term_mode Bottom;
-val rewrite_term_top = rewrite_term_mode Top;
+val rewrite_term_topdown = rewrite_term_mode Top;
 val rewrite_term_yoyo = rewrite_term_mode Yoyo;
 
 end;