diff -r b19373bd7ea8 -r a29aefc88c8d src/Doc/ProgProve/LaTeXsugar.thy
--- a/src/Doc/ProgProve/LaTeXsugar.thy	Thu Mar 06 12:58:51 2014 +0100
+++ b/src/Doc/ProgProve/LaTeXsugar.thy	Thu Mar 06 13:44:01 2014 +0100
@@ -46,7 +46,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