# HG changeset patch
# User wenzelm
# Date 1447181456 -3600
# Node ID e8fcd347b6699d07b87ee2b0ef2ac64969519dfd
# Parent  34978e1b234ff28343910a4e1473a0acecac7fd6
ignore pointless/unused options;

diff -r 34978e1b234f -r e8fcd347b669 src/Doc/antiquote_setup.ML
--- 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);