diff -r 90def2b06305 -r 1a279ad4c6a4 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Fri Jan 19 19:09:25 2018 +0100 +++ b/src/Pure/Thy/thy_output.ML Fri Jan 19 19:41:28 2018 +0100 @@ -99,8 +99,10 @@ let val body = Symbol_Pos.cartouche_content syms; val source = Input.source true (Symbol_Pos.implode body) (Symbol_Pos.range body); + val ctxt' = ctxt + |> Config.put Document_Antiquotation.thy_output_display false; in - output_text ctxt {markdown = false} source + output_text ctxt' {markdown = false} source |> Latex.enclose_body "%\n\\isamarkupcmt{" "%\n}" end | (SOME Comment.Cancel, _) =>