--- a/src/Doc/antiquote_setup.ML Fri Jan 19 11:26:31 2018 +0100
+++ b/src/Doc/antiquote_setup.ML Fri Jan 19 11:34:41 2018 +0100
@@ -127,8 +127,7 @@
Output.output
(Document_Antiquotation.format ctxt
(Document_Antiquotation.quote ctxt (Thy_Output.pretty_thm ctxt thm))) ^
- enclose "\\rulename{" "}"
- (Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name))))
+ enclose "\\rulename{" "}" (Output.output name))
#> space_implode "\\par\\smallskip%\n"
#> Latex.string #> single
#> Thy_Output.isabelle ctxt));
--- a/src/Pure/Thy/document_antiquotations.ML Fri Jan 19 11:26:31 2018 +0100
+++ b/src/Pure/Thy/document_antiquotations.ML Fri Jan 19 11:34:41 2018 +0100
@@ -296,7 +296,7 @@
(Thy_Output.antiquotation_pretty \<^binding>\<open>doc\<close> (Scan.lift (Parse.position Parse.embedded))
(fn ctxt => fn (name, pos) =>
let val _ = Context_Position.report ctxt pos (Markup.doc name)
- in [Thy_Output.pretty_text ctxt name] end));
+ in [Pretty.str name] end));
(* formal entities *)