tuned;
authorwenzelm
Sun, 24 Dec 2023 11:58:33 +0100
changeset 79346 f86c310327df
parent 79345 75701d767ed9
child 79347 8aca79b3a9cb
tuned;
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 *)