diff -r deb9b0283259 -r 998e01d6f8fd src/Doc/antiquote_setup.ML
--- a/src/Doc/antiquote_setup.ML	Tue Jan 09 15:18:41 2018 +0100
+++ b/src/Doc/antiquote_setup.ML	Tue Jan 09 15:40:12 2018 +0100
@@ -73,7 +73,7 @@
 fun prep_ml source =
   (Input.source_content source, ML_Lex.read_source false source);
 
-fun index_ml name kind ml = Thy_Output.antiquotation name
+fun index_ml name kind ml = Document_Antiquotation.setup name
   (Scan.lift (Args.text_input -- Scan.option (Args.colon |-- Args.text_input)))
   (fn {context = ctxt, ...} => fn (source1, opt_source2) =>
     let
@@ -119,17 +119,18 @@
 (* named theorems *)
 
 val _ =
-  Theory.setup (Thy_Output.antiquotation @{binding named_thms}
+  Theory.setup (Document_Antiquotation.setup @{binding named_thms}
     (Scan.repeat (Attrib.thm -- Scan.lift (Args.parens Args.name)))
     (fn {context = ctxt, ...} =>
       map (apfst (Thy_Output.pretty_thm ctxt))
-      #> (if Config.get ctxt Thy_Output.quotes then map (apfst Pretty.quote) else I)
-      #> (if Config.get ctxt Thy_Output.display
+      #> (if Config.get ctxt Document_Antiquotation.thy_output_quotes
+          then map (apfst Pretty.quote) else I)
+      #> (if Config.get ctxt Document_Antiquotation.thy_output_display
           then
             map (fn (p, name) =>
               Output.output
                 (Thy_Output.string_of_margin ctxt
-                  (Pretty.indent (Config.get ctxt Thy_Output.indent) p)) ^
+                  (Pretty.indent (Config.get ctxt Document_Antiquotation.thy_output_indent) p)) ^
               "\\rulename{" ^
               Output.output (Pretty.unformatted_string_of (Thy_Output.pretty_text ctxt name)) ^ "}")
             #> space_implode "\\par\\smallskip%\n"
@@ -160,7 +161,7 @@
 val arg = enclose "{" "}" o clean_string;
 
 fun entity check markup binding index =
-  Thy_Output.antiquotation
+  Document_Antiquotation.setup
     (binding |> Binding.map_name (fn name => name ^
       (case index of NONE => "" | SOME true => "_def" | SOME false => "_ref")))
     (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Parse.position Args.name))
@@ -204,8 +205,8 @@
     entity_antiqs no_check "" @{binding fact} #>
     entity_antiqs no_check "" @{binding variable} #>
     entity_antiqs no_check "" @{binding case} #>
-    entity_antiqs Thy_Output.check_command "" @{binding antiquotation} #>
-    entity_antiqs Thy_Output.check_option "" @{binding antiquotation_option} #>
+    entity_antiqs Document_Antiquotation.check "" @{binding antiquotation} #>
+    entity_antiqs Document_Antiquotation.check_option "" @{binding antiquotation_option} #>
     entity_antiqs no_check "isasystem" @{binding setting} #>
     entity_antiqs check_system_option "isasystem" @{binding system_option} #>
     entity_antiqs no_check "" @{binding inference} #>