clarified context;
authorwenzelm
Sun, 23 May 2021 17:08:34 +0200
changeset 73766 e502b40717c7
parent 73765 ebaed09ce06e
child 73767 b49a03bb136c
clarified context;
src/Pure/Thy/document_antiquotations.ML
--- 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);