# HG changeset patch
# User wenzelm
# Date 1729533747 -7200
# Node ID 274344c65e018153fbad0ed3c6d8f53b4d2372ef
# Parent  3d09d6f4c5b1cef75f86ccdb3ec55106aff543cb
tuned;

diff -r 3d09d6f4c5b1 -r 274344c65e01 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Oct 21 14:50:59 2024 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Oct 21 20:02:27 2024 +0200
@@ -668,16 +668,14 @@
     val Mode {abbrev, ...} = get_mode ctxt;
 
     val nets = Consts.revert_abbrevs consts (print_mode_value () @ [""]);
-    fun retrieves t =
+    fun match_abbrev t =
       let
         val retrieve =
           if Term.could_beta_eta_contract t
           then Item_Net.retrieve
           else Item_Net.retrieve_matching;
-      in maps (fn net => retrieve net t) nets end;
-
-    fun match_abbrev t =
-      Option.map #1 (get_first (Pattern.match_rew thy t) (retrieves t));
+        fun match_rew net = get_first (Pattern.match_rew thy t) (retrieve net t);
+      in Option.map #1 (get_first match_rew nets) end;
   in
     if abbrev orelse not (Config.get ctxt show_abbrevs) orelse not (can Term.type_of tm) then tm
     else Pattern.rewrite_term_top thy [] [match_abbrev] tm