
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 \<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 " ::",




