src/HOL/Library/LaTeXsugar.thy
changeset 69081 0b403ce1e8f8
parent 67505 ceb324e34c14
child 69592 a80d8ec6c998
     1.1 --- a/src/HOL/Library/LaTeXsugar.thy	Sat Sep 29 17:08:07 2018 +0200
     1.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Sat Sep 29 21:02:04 2018 +0200
     1.3 @@ -99,7 +99,7 @@
     1.4  setup \<open>
     1.5    Thy_Output.antiquotation_pretty_source \<^binding>\<open>const_typ\<close> (Scan.lift Args.embedded_inner_syntax)
     1.6      (fn ctxt => fn c =>
     1.7 -      let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c in
     1.8 +      let val tc = Proof_Context.read_const {proper = false, strict = false} ctxt c in
     1.9          Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
    1.10            Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
    1.11        end)