# HG changeset patch
# User wenzelm
# Date 1516358081 -3600
# Node ID aa8c25c528c0d7cad7b6854ae8f8820e09f9e2d1
# Parent  482b62d694ca4c8aed0fc7652f370b5acfd82db6
tuned output of plain name;

diff -r 482b62d694ca -r aa8c25c528c0 src/Doc/antiquote_setup.ML
--- 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));
diff -r 482b62d694ca -r aa8c25c528c0 src/Pure/Thy/document_antiquotations.ML
--- 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 *)