diff -r f4be1b0d7a51 -r ef1a18e20ace src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Fri May 21 11:19:53 2021 +0200
+++ b/src/Doc/Main/Main_Doc.thy	Fri May 21 12:29:29 2021 +0200
@@ -4,14 +4,14 @@
 begin
 
 setup \<open>
-  Thy_Output.antiquotation_pretty_source \<^binding>\<open>term_type_only\<close> (Args.term -- Args.typ_abbrev)
+  Document_Output.antiquotation_pretty_source \<^binding>\<open>term_type_only\<close> (Args.term -- Args.typ_abbrev)
     (fn ctxt => fn (t, T) =>
       (if fastype_of t = Sign.certify_typ (Proof_Context.theory_of ctxt) T then ()
        else error "term_type_only: type mismatch";
        Syntax.pretty_typ ctxt T))
 \<close>
 setup \<open>
-  Thy_Output.antiquotation_pretty_source \<^binding>\<open>expanded_typ\<close> Args.typ
+  Document_Output.antiquotation_pretty_source \<^binding>\<open>expanded_typ\<close> Args.typ
     Syntax.pretty_typ
 \<close>
 (*>*)