src/Doc/Prog_Prove/LaTeXsugar.thy

   ("\<^latex>\<open>{\\normalsize{}\<close>If\<^latex>\<open>\\,}\<close> _ /\<^latex>\<open>{\\normalsize \\,\<close>then\<^latex>\<open>\\,}\<close>/ _.")
   "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^latex>\<open>{\\normalsize \\,\<close>and\<^latex>\<open>\\,}\<close>/ _")
   "_asm" :: "prop \<Rightarrow> asms" ("_")
 
 setup \<open>
-  Thy_Output.antiquotation_pretty_source \<^binding>\<open>const_typ\<close> (Scan.lift Args.embedded_inner_syntax)
+  Document_Output.antiquotation_pretty_source \<^binding>\<open>const_typ\<close>
+    (Scan.lift Args.embedded_inner_syntax)
     (fn ctxt => fn c =>
       let val tc = Proof_Context.read_const {proper = false, strict = false} ctxt c in
-        Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
+        Pretty.block [Document_Output.pretty_term ctxt tc, Pretty.str " ::",
           Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
       end)
 \<close>
 
 end