# HG changeset patch
# User wenzelm
# Date 1621782514 -7200
# Node ID e502b40717c76bc32702d7f6c50c6ea2c3abd2f3
# Parent  ebaed09ce06e32ebd9fcbbefaefdd26fbb08047f
clarified context;

diff -r ebaed09ce06e -r e502b40717c7 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);