src/HOL/Library/LaTeXsugar.thy
changeset 67505 ceb324e34c14
parent 67463 a5ca98950a91
child 69081 0b403ce1e8f8
     1.1 --- a/src/HOL/Library/LaTeXsugar.thy	Thu Jan 25 11:29:52 2018 +0100
     1.2 +++ b/src/HOL/Library/LaTeXsugar.thy	Thu Jan 25 14:13:55 2018 +0100
     1.3 @@ -100,8 +100,8 @@
     1.4    Thy_Output.antiquotation_pretty_source \<^binding>\<open>const_typ\<close> (Scan.lift Args.embedded_inner_syntax)
     1.5      (fn ctxt => fn c =>
     1.6        let val tc = Proof_Context.read_const {proper = true, strict = false} ctxt c in
     1.7 -        [Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
     1.8 -          Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]]
     1.9 +        Pretty.block [Thy_Output.pretty_term ctxt tc, Pretty.str " ::",
    1.10 +          Pretty.brk 1, Syntax.pretty_typ ctxt (fastype_of tc)]
    1.11        end)
    1.12  \<close>
    1.13