diff -r 3a5d33e8a019 -r 37aa898e0523 doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Fri Nov 02 16:38:37 2007 +0100
+++ b/doc-src/IsarRef/syntax.tex	Fri Nov 02 18:52:57 2007 +0100
@@ -526,7 +526,7 @@
 
 \item [$\at\{term~t\}$] prints a well-typed term $t$.
 
-\item [$\at\{const~c\}$] prints a well-defined constant $c$.
+\item [$\at\{const~c\}$] prints a logical or syntactic constant $c$.
   
 \item [$\at\{abbrev~c\,\vec x\}$] prints a constant abbreviation
   $c\,\vec x \equiv rhs$ as defined in the current context.