--- a/src/Doc/antiquote_setup.ML Tue Nov 10 19:03:29 2015 +0100
+++ b/src/Doc/antiquote_setup.ML Tue Nov 10 19:50:56 2015 +0100
@@ -253,10 +253,7 @@
idx ^
(Output.output name
|> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
- |> (if Config.get ctxt Thy_Output.quotes then quote else I)
- |> (if Config.get ctxt Thy_Output.display
- then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
- else hyper o enclose "\\mbox{\\isa{" "}}"))
+ |> hyper o enclose "\\mbox{\\isa{" "}}")
else error ("Bad " ^ kind ^ " " ^ quote name ^ Position.here pos)
end);