--- a/src/HOL/Library/LaTeXsugar.thy Thu Jan 03 22:30:41 2019 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy Fri Jan 04 21:49:06 2019 +0100
@@ -97,7 +97,8 @@
"_asm" :: "prop \<Rightarrow> asms" ("_")
setup \<open>
- Thy_Output.antiquotation_pretty_source \<^binding>\<open>const_typ\<close> (Scan.lift Args.embedded_inner_syntax)
+ Thy_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 " ::",