src/HOL/Library/LaTeXsugar.thy

--- a/src/HOL/Library/LaTeXsugar.thy	Thu Mar 06 12:58:51 2014 +0100
+++ b/src/HOL/Library/LaTeXsugar.thy	Thu Mar 06 13:44:01 2014 +0100
@@ -100,7 +100,7 @@
 setup{*
   let
     fun pretty ctxt c =
-      let val tc = Proof_Context.read_const_proper ctxt false c
+      let val tc = Proof_Context.read_const ctxt {proper = true, strict = false} dummyT c
       in Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
             Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
       end