--- a/src/HOL/Library/LaTeXsugar.thy Wed Oct 20 20:04:28 2021 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy Wed Oct 20 20:25:33 2021 +0200
@@ -98,7 +98,7 @@
setup \<open>
Document_Output.antiquotation_pretty_source_embedded \<^binding>\<open>const_typ\<close>
- (Scan.lift Args.embedded_inner_syntax)
+ (Scan.lift Parse.embedded_inner_syntax)
(fn ctxt => fn c =>
let val tc = Proof_Context.read_const {proper = false, strict = false} ctxt c in
Pretty.block [Document_Output.pretty_term ctxt tc, Pretty.str " ::",