diff -r 620db300c038 -r 57753e0ec1d4 doc-src/TutorialI/Sets/sets.tex
--- a/doc-src/TutorialI/Sets/sets.tex	Sat Mar 21 12:37:13 2009 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex	Sun Mar 22 19:36:04 2009 +0100
@@ -299,7 +299,7 @@
 \isa{UN x:A.\ B} in \textsc{ascii}. Indexed union satisfies this basic law:
 \begin{isabelle}
 (b\ \isasymin\
-(\isasymUnion x\isasymin A. B\ x) =\ (\isasymexists x\isasymin A.\
+(\isasymUnion x\isasymin A. B\ x)) =\ (\isasymexists x\isasymin A.\
 b\ \isasymin\ B\ x)
 \rulenamedx{UN_iff}
 \end{isabelle}
@@ -414,12 +414,12 @@
 $k$-element subsets of~$A$ is \index{binomial coefficients}
 $\binom{n}{k}$.
 
-\begin{warn}
-The term \isa{finite\ A} is defined via a syntax translation as an
-abbreviation for \isa{A {\isasymin} Finites}, where the constant
-\cdx{Finites} denotes the set of all finite sets of a given type.  There
-is no constant \isa{finite}.
-\end{warn}
+%\begin{warn}
+%The term \isa{finite\ A} is defined via a syntax translation as an
+%abbreviation for \isa{A {\isasymin} Finites}, where the constant
+%\cdx{Finites} denotes the set of all finite sets of a given type.  There
+%is no constant \isa{finite}.
+%\end{warn}
 \index{sets|)}