--- a/src/Doc/Sugar/Sugar.thy Sat Sep 29 17:08:07 2018 +0200
+++ b/src/Doc/Sugar/Sugar.thy Sat Sep 29 21:02:04 2018 +0200
@@ -117,6 +117,18 @@
hidden.
+\section{Printing constants and their type}
+
+Instead of
+\verb!@!\verb!{const myconst}! \verb!@!\verb!{text "::"}! \verb!@!\verb!{typeof myconst}!,
+you can write \verb!@!\verb!{const_typ myconst}! using the new antiquotation
+\texttt{const\_typ} defined in \texttt{LaTeXsugar}. For example,
+\verb!@!\verb!{const_typ length}! produces @{const_typ length} (see below for how to suppress
+the question mark).
+This works both for genuine constants and for variables fixed in some context,
+especially in a locale.
+
+
\section{Printing theorems}
The @{prop "P \<Longrightarrow> Q \<Longrightarrow> R"} syntax is a bit idiosyncratic. If you would like
@@ -564,16 +576,6 @@
\end{quote}
The \texttt{isabelle} environment is the one defined in the standard file
\texttt{isabelle.sty} which most likely you are loading anyway.
-
-
-\section{Antiquotation}
-
-You want to show a constant and its type? Instead of going
-\verb!@!\verb!{const myconst}! \verb!@!\verb!{text "::"}! \verb!@!\verb!{typeof myconst}!,
-you can just write \verb!@!\verb!{const_typ myconst}! using the new antiquotation
-\texttt{const\_typ} defined in \texttt{LaTeXsugar}. For example,
-\verb!@!\verb!{const_typ length}! produces @{const_typ length}.
-
\<close>
(*<*)
--- a/src/HOL/Library/LaTeXsugar.thy Sat Sep 29 17:08:07 2018 +0200
+++ b/src/HOL/Library/LaTeXsugar.thy Sat Sep 29 21:02:04 2018 +0200
@@ -99,7 +99,7 @@
setup \<open>
Thy_Output.antiquotation_pretty_source \<^binding>\<open>const_typ\<close> (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)