doc-src/Logics/ZF.tex

--- a/doc-src/Logics/ZF.tex	Wed Apr 29 11:46:42 1998 +0200
+++ b/doc-src/Logics/ZF.tex	Thu Apr 30 17:16:25 1998 +0200
@@ -1779,7 +1779,7 @@
 step, provided we somehow supply it with~\texttt{prem}.  We can add
 \hbox{\tt prem RS subsetD} to the claset as an introduction rule:
 \begin{ttbox}
-by (blast_tac (!claset addIs [prem RS subsetD]) 1);
+by (blast_tac (claset() addIs [prem RS subsetD]) 1);
 {\out Depth = 0}
 {\out Depth = 1}
 {\out Depth = 2}