# HG changeset patch
# User wenzelm
# Date 1684610624 -7200
# Node ID 3fde7a52c650621b698b239972df09284e6759e7
# Parent  90b64ffc48a35170a90913aab2d6d1afd5825321
tuned --- Token.make_string / Token.assign are value-oriented;

diff -r 90b64ffc48a3 -r 3fde7a52c650 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sat May 20 20:56:13 2023 +0200
+++ b/src/Pure/Isar/attrib.ML	Sat May 20 21:23:44 2023 +0200
@@ -248,12 +248,9 @@
       Scan.lift Args.internal_declaration >> (Thm.declaration_attribute o K o Morphism.form))
     "internal attribute");
 
-val internal_attribute_name =
-  internal_name (Context.the_local_context ()) "attribute";
-
-fun internal_source value =
-  internal_attribute_name ::
-    [Token.make_string ("<attribute>", Position.none) |> Token.assign (SOME value)];
+val internal_name = internal_name (Context.the_local_context ()) "attribute";
+val internal_arg = Token.make_string ("<attribute>", Position.none);
+fun internal_source value = [internal_name, Token.assign (SOME value) internal_arg];
 
 in