tuned;
authorwenzelm
Mon, 21 Oct 2024 20:02:27 +0200
changeset 81221 274344c65e01
parent 81220 3d09d6f4c5b1
child 81222 b61abd1e5027
tuned;
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