# HG changeset patch
# User nipkow
# Date 1538247932 -7200
# Node ID 0405d06f08f31237865a72cc4b168746e491bfd5
# Parent  0b403ce1e8f8721f7a00d2717f64365e890cf6d9
adapted to Library/LaTeXsugar

diff -r 0b403ce1e8f8 -r 0405d06f08f3 src/Doc/Prog_Prove/LaTeXsugar.thy
--- a/src/Doc/Prog_Prove/LaTeXsugar.thy	Sat Sep 29 21:02:04 2018 +0200
+++ b/src/Doc/Prog_Prove/LaTeXsugar.thy	Sat Sep 29 21:05:32 2018 +0200
@@ -46,7 +46,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)