# HG changeset patch
# User wenzelm
# Date 1703706753 -3600
# Node ID c5282516e2d55a5e273ad7768556165e3c75d3d6
# Parent  b275e3379024f0f7875547e9e635947b7d3abe2e
tuned;

diff -r b275e3379024 -r c5282516e2d5 src/Pure/thm_name.ML
--- a/src/Pure/thm_name.ML	Wed Dec 27 20:40:15 2023 +0100
+++ b/src/Pure/thm_name.ML	Wed Dec 27 20:52:33 2023 +0100
@@ -34,6 +34,6 @@
 fun list (name, pos: Position.T) [thm] = [(((name, 0): T, pos), thm)]
   | list (name, pos) thms = map_index (fn (i, thm) => (((name, i + 1), pos), thm)) thms;
 
-fun expr name = split_list #>> burrow (list name) #> op ~~;
+fun expr name = burrow_fst (burrow (list name));
 
 end;