--- a/src/HOL/Library/LaTeXsugar.thy Sat Sep 29 17:08:07 2018 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy Sat Sep 29 21:02:04 2018 +0200
@@ -99,7 +99,7 @@
setup \<open>
Thy_Output.antiquotation_pretty_source \<^binding>\<open>const_typ\<close> (Scan.lift Args.embedded_inner_syntax)
(fn ctxt => fn c =>
- let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c in
+ let val tc = Proof_Context.read_const {proper = false, strict = false} ctxt c in
Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
end)