# HG changeset patch
# User wenzelm
# Date 1703415513 -3600
# Node ID f86c310327dfd723ce6aa150dcdfd74ad1a3e50e
# Parent  75701d767ed9b63a0f76b274489d4114be1b14a2
tuned;

diff -r 75701d767ed9 -r f86c310327df src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun Dec 24 11:51:59 2023 +0100
+++ b/src/Pure/Isar/attrib.ML	Sun Dec 24 11:58:33 2023 +0100
@@ -181,10 +181,10 @@
 
 (* attributed declarations *)
 
-fun map_specs f = map (apfst (apsnd f));
+fun map_specs f = (map o apfst o apsnd) f;
 
-fun map_facts f = map (apfst (apsnd f) o apsnd (map (apsnd f)));
-fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g)));
+fun map_facts f = map (fn (a, b) => (apsnd f a, (map o apsnd) f b));
+fun map_facts_refs f g = map_facts f #> (map o apsnd o map o apfst) g;
 
 
 (* implicit context *)