diff -r 54a7b9422d3e -r c82c7b78b509 src/Doc/Prog_Prove/Logic.thy
--- 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}