diff -r 8403bd51f8b1 -r 042041c0ebeb src/HOL/Library/LaTeXsugar.thy --- 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 \ Document_Output.antiquotation_pretty_source_embedded \<^binding>\const_typ\ - (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 " ::",