changeset 56002 | 2028467b4df4 |
parent 55955 | e8f1bf005661 |
child 56245 | 84fc7dfa3cd4 |
--- a/src/Doc/ProgProve/LaTeXsugar.thy Sun Mar 09 15:21:08 2014 +0100 +++ b/src/Doc/ProgProve/LaTeXsugar.thy Sun Mar 09 16:37:56 2014 +0100 @@ -46,7 +46,7 @@ setup{* let fun pretty ctxt c = - let val tc = Proof_Context.read_const ctxt {proper = true, strict = false} c + let val tc = Proof_Context.read_const {proper = true, 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