# HG changeset patch
# User wenzelm
# Date 1682105110 -7200
# Node ID e7fd273657f188536c1a1f6aa0405ba04ad6b5f3
# Parent  38d0a90e87c156638e5be8c417e8d6d220e128bf
tuned;

diff -r 38d0a90e87c1 -r e7fd273657f1 src/Pure/Tools/named_theorems.ML
--- a/src/Pure/Tools/named_theorems.ML	Fri Apr 21 21:12:26 2023 +0200
+++ b/src/Pure/Tools/named_theorems.ML	Fri Apr 21 21:25:10 2023 +0200
@@ -59,7 +59,7 @@
 
 fun clear name = map_entry name (K Thm.item_net);
 
-fun add_thm name th = map_entry name (Item_Net.update (Thm.trim_context th));
+fun add_thm name = map_entry name o Item_Net.update o Thm.trim_context;
 fun del_thm name = map_entry name o Item_Net.remove;
 
 val add = Thm.declaration_attribute o add_thm;