tuned --- Token.make_string / Token.assign are value-oriented;

--- 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