# HG changeset patch
# User wenzelm
# Date 1729515059 -7200
# Node ID 3d09d6f4c5b1cef75f86ccdb3ec55106aff543cb
# Parent  2554f664deac268006b455f574fe7cb5901581ab
clarified signature;

diff -r 2554f664deac -r 3d09d6f4c5b1 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Mon Oct 21 14:33:59 2024 +0200
+++ b/src/Pure/Isar/proof_context.ML	Mon Oct 21 14:50:59 2024 +0200
@@ -661,16 +661,26 @@
 
 val show_abbrevs = Config.declare_bool ("show_abbrevs", \<^here>) (K true);
 
-fun contract_abbrevs ctxt t =
+fun contract_abbrevs ctxt tm =
   let
     val thy = theory_of ctxt;
     val consts = consts_of ctxt;
     val Mode {abbrev, ...} = get_mode ctxt;
-    val retrieve = Consts.retrieve_abbrevs consts (print_mode_value () @ [""]);
-    fun match_abbrev u = Option.map #1 (get_first (Pattern.match_rew thy u) (retrieve u));
+
+    val nets = Consts.revert_abbrevs consts (print_mode_value () @ [""]);
+    fun retrieves 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));
   in
-    if abbrev orelse not (Config.get ctxt show_abbrevs) orelse not (can Term.type_of t) then t
-    else Pattern.rewrite_term_top thy [] [match_abbrev] t
+    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
   end;
 
 
diff -r 2554f664deac -r 3d09d6f4c5b1 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Mon Oct 21 14:33:59 2024 +0200
+++ b/src/Pure/consts.ML	Mon Oct 21 14:50:59 2024 +0200
@@ -11,7 +11,7 @@
   val eq_consts: T * T -> bool
   val change_base: bool -> T -> T
   val change_ignore: T -> T
-  val retrieve_abbrevs: T -> string list -> term -> (term * term) list
+  val revert_abbrevs: T -> string list -> (term * term) Item_Net.T list
   val dest: T ->
    {const_space: Name_Space.T,
     constants: (string * (typ * term option)) list,
@@ -85,16 +85,8 @@
 fun update_abbrevs mode abbrs =
   Symtab.map_default (mode, empty_abbrevs) (Item_Net.update abbrs);
 
-fun retrieve_abbrevs (Consts {rev_abbrevs, ...}) modes =
-  let val nets = map_filter (Symtab.lookup rev_abbrevs) modes in
-    fn 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
-  end;
+fun revert_abbrevs (Consts {rev_abbrevs, ...}) modes =
+  map_filter (Symtab.lookup rev_abbrevs) modes;
 
 
 (* dest consts *)