src/HOL/Library/LaTeXsugar.thy
changeset 69592 a80d8ec6c998
parent 69081 0b403ce1e8f8
child 69593 3dda49e08b9d
     1.1 --- a/src/HOL/Library/LaTeXsugar.thy	Thu Jan 03 22:30:41 2019 +0100
     1.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Fri Jan 04 21:49:06 2019 +0100
     1.3 @@ -97,7 +97,8 @@
     1.4    "_asm" :: "prop \<Rightarrow> asms" ("_")
     1.5  
     1.6  setup \<open>
     1.7 -  Thy_Output.antiquotation_pretty_source \<^binding>\<open>const_typ\<close> (Scan.lift Args.embedded_inner_syntax)
     1.8 +  Thy_Output.antiquotation_pretty_source_embedded \<^binding>\<open>const_typ\<close>
     1.9 +    (Scan.lift Args.embedded_inner_syntax)
    1.10      (fn ctxt => fn c =>
    1.11        let val tc = Proof_Context.read_const {proper = false, strict = false} ctxt c in
    1.12          Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",