--- a/src/Doc/Prog_Prove/Logic.thy Tue Feb 09 11:05:53 2016 +0100
+++ b/src/Doc/Prog_Prove/Logic.thy Tue Feb 09 16:38:43 2016 +0100
@@ -134,7 +134,7 @@
\begin{tabular}{l@ {\quad}l}
@{const_typ set}\index{set@@{const set}} & converts a list to the set of its elements\\
@{const_typ finite}\index{finite@@{const finite}} & is true iff its argument is finite\\
-@{const_typ card}\index{card@@{const card}} & is the cardinality of a finite set\\
+\noquotes{@{term[source] "card :: 'a set \<Rightarrow> nat"}}\index{card@@{const card}} & is the cardinality of a finite set\\
& and is @{text 0} for all infinite sets\\
@{thm image_def}\index{$IMP042@@{term"f ` A"}} & is the image of a function over a set
\end{tabular}