--- a/src/Pure/Thy/document_antiquotations.ML Sat May 22 22:58:10 2021 +0200
+++ b/src/Pure/Thy/document_antiquotations.ML Sun May 23 17:08:34 2021 +0200
@@ -368,7 +368,7 @@
val ctxt' = Config.put Document_Antiquotation.thy_output_display false ctxt;
val kind' = if kind = "" then " (ML)" else " (ML " ^ kind ^ ")";
val txt' = Latex.block [Document_Output.verbatim ctxt' txt1, Latex.string kind'];
- val like = Document_Antiquotation.approx_content ctxt source1;
+ val like = Document_Antiquotation.approx_content ctxt' source1;
in Latex.index_entry {items = [{text = txt', like = like}], def = def} end);
in Latex.block (the_list index_text @ [main_text]) end);