# 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 \ Thy_Output.antiquotation_pretty_source \<^binding>\const_typ\ (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)