src/Pure/Thy/latex.ML
changeset 76957 deb7dffb3340
parent 76956 e47fb5cfef41
child 77768 65008644d394
--- a/src/Pure/Thy/latex.ML	Thu Jan 12 19:48:47 2023 +0100
+++ b/src/Pure/Thy/latex.ML	Thu Jan 12 20:09:08 2023 +0100
@@ -206,8 +206,8 @@
         if exists_string (fn c => c = ",") s
         then error ("Single citation expected, without commas" ^ Position.here pos)
         else ());
-    val citation = space_implode "," (map #1 citations);
-    val markup = Markup.latex_cite {kind = kind, citation = citation};
+    val citations' = space_implode "," (map #1 citations);
+    val markup = Markup.latex_cite {kind = kind, citations = citations'};
   in [XML.Elem (markup, location)] end;