prefer rewrite_term_yoyo for improved performance and occasionally better results (conforming to Ast.normalize);

--- a/NEWS	Thu Oct 24 12:44:48 2024 +0200
+++ b/NEWS	Thu Oct 24 22:05:57 2024 +0200
@@ -57,6 +57,12 @@
 work in the same manner, but more complex translations may require
 manual changes: rare INCOMPATIBILITY.
 
+* Printing term abbreviations now uses a different strategy: alternate
+top-down, bottom-up, top-down etc. until a normal form is reached. This
+is more efficient than the former top-down strategy. It also conforms to
+AST rewriting (command 'translations'). Rare INCOMPATIBILITY, slightly
+different results could be printed (often slightly "better" ones).
+
 * The Simplifier now supports special "congprocs", using keyword
 'congproc' or 'weak_congproc' in the 'simproc_setup' command (or ML
 antiquotation of the same name). See also
@@ -160,6 +166,12 @@
 
 *** ML ***
 
+* The new operation Pattern.rewrite_term_yoyo alternates top-down,
+bottom-up, top-down etc. until a normal form is reached. This often
+works better than former rewrite_term_top --- that is still available,
+but has been renamed to rewrite_term_topdown to emphasize that something
+notable has changed here.
+
 * Constructors for type Pretty.T (such as Pretty.str, Pretty.mark_str,
 Pretty.markup_block) are now value-oriented. Use of the global
 print_mode is restricted to ultimate Pretty.string_of (and some

--- a/src/HOL/Library/adhoc_overloading.ML	Thu Oct 24 12:44:48 2024 +0200
+++ b/src/HOL/Library/adhoc_overloading.ML	Thu Oct 24 22:05:57 2024 +0200
@@ -173,7 +173,7 @@
       |> get_overloaded ctxt
       |> Option.map (Const o rpair (Term.type_of t));
   in
-    Pattern.rewrite_term_top (Proof_Context.theory_of ctxt) [] [proc]
+    Pattern.rewrite_term_yoyo (Proof_Context.theory_of ctxt) [] [proc]
   end;
 
 fun check ctxt =

--- a/src/Pure/Isar/class.ML	Thu Oct 24 12:44:48 2024 +0200
+++ b/src/Pure/Isar/class.ML	Thu Oct 24 22:05:57 2024 +0200
@@ -447,7 +447,7 @@
 fun canonical_abbrev_target class phi prmode ((b, mx), rhs) lthy =
   let
     val thy = Proof_Context.theory_of lthy;
-    val preprocess = perhaps (try (Pattern.rewrite_term_top thy (these_unchecks thy [class]) []));
+    val preprocess = perhaps (try (Pattern.rewrite_term_yoyo thy (these_unchecks thy [class]) []));
     val (global_rhs, (_, (_, term_params))) =
       Generic_Target.export_abbrev lthy preprocess rhs;
     val mx' = Generic_Target.check_mixfix_global (b, null term_params) mx;
@@ -469,7 +469,7 @@
     val thy = Proof_Context.theory_of lthy;
     val phi = morphism lthy class;
     val rhs_generic =
-      perhaps (try (Pattern.rewrite_term_top thy (these_unchecks_reversed thy [class]) [])) rhs;
+      perhaps (try (Pattern.rewrite_term_yoyo thy (these_unchecks_reversed thy [class]) [])) rhs;
   in
     lthy
     |> canonical_abbrev_target class phi prmode ((b, mx), rhs)

--- a/src/Pure/Isar/overloading.ML	Thu Oct 24 12:44:48 2024 +0200
+++ b/src/Pure/Isar/overloading.ML	Thu Oct 24 22:05:57 2024 +0200
@@ -92,7 +92,7 @@
   end;
 
 fun rewrite_liberal thy unchecks t =
-  (case try (Pattern.rewrite_term_top thy unchecks []) t of
+  (case try (Pattern.rewrite_term_yoyo thy unchecks []) t of
     NONE => NONE
   | SOME t' => if t aconv t' then NONE else SOME t');
 

--- a/src/Pure/Isar/proof_context.ML	Thu Oct 24 12:44:48 2024 +0200
+++ b/src/Pure/Isar/proof_context.ML	Thu Oct 24 22:05:57 2024 +0200
@@ -677,7 +677,7 @@
         fun match_abbrev t = get_first (fn net => get_first (rew t) (Item_Net.retrieve net t)) nets;
       in
         Term_Subst.instantiate inst tm
-        |> Pattern.rewrite_term_top thy [] [match_abbrev]
+        |> Pattern.rewrite_term_yoyo thy [] [match_abbrev]
         |> Term_Subst.instantiate_frees (Variable.import_inst_revert inst)
       end
   end;

--- 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;