--- a/doc-src/TutorialI/fp.tex Thu Nov 29 13:33:45 2001 +0100
+++ b/doc-src/TutorialI/fp.tex Thu Nov 29 14:12:42 2001 +0100
@@ -412,7 +412,7 @@
In HOL it must be ruled out because it requires a type
\isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the
same cardinality --- an impossibility. For the same reason it is not possible
-to allow recursion involving the type \isa{set}, which is isomorphic to
+to allow recursion involving the type \isa{t set}, which is isomorphic to
\isa{t \isasymFun\ bool}.
Fortunately, a limited form of recursion