diff -r 669f47397249 -r 276ad4354069 src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Sun Dec 20 13:03:41 2015 +0100
+++ b/src/Doc/antiquote_setup.ML	Sun Dec 20 13:06:26 2015 +0100
@@ -130,13 +130,15 @@
               Output.output
                 (Thy_Output.string_of_margin ctxt
                   (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^
-              "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
+              "\\rulename{" ^
+              Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)) ^ "}")
             #> space_implode "\\par\\smallskip%\n"
             #> Latex.environment "isabelle"
           else
             map (fn (p, name) =>
-              Output.output (Pretty.str_of p) ^
-              "\\rulename{" ^ Output.output (Pretty.str_of (Thy_Output.pretty_text ctxt name)) ^ "}")
+              Output.output (Pretty.unformatted_string_of p) ^
+              "\\rulename{" ^
+              Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)) ^ "}")
             #> space_implode "\\par\\smallskip%\n"
             #> enclose "\\isa{" "}")));