--- a/src/HOL/Library/LaTeXsugar.thy Fri May 21 11:19:53 2021 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy Fri May 21 12:29:29 2021 +0200
@@ -97,11 +97,11 @@
"_asm" :: "prop \<Rightarrow> asms" ("_")
setup \<open>
- Thy_Output.antiquotation_pretty_source_embedded \<^binding>\<open>const_typ\<close>
+ Document_Output.antiquotation_pretty_source_embedded \<^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>