Revert 'Consistent use of "failure" instead of "failure occurs".'

This reverts commit 15eb27a.

"Failure occurs if ..." is more grammatical than "Failure if ...".
There are some existing occurrences of the latter that still need to
be fixed.

Manual/Description/system.tex

@@ -1289,7 +1289,7 @@ \subsection{Type instantiation}
 \ml{INST\_TYPE[$\alpha_1$~|->~$\sigma_1$%
   ,$\ldots$,$\alpha_n$~|->~$\sigma_n$]~$th$} returns the result of
 instantiating each occurrence of $\alpha_i$ in the theorem $th$ to
-$\sigma_i$ (for $1 \leq i \leq n$). Failure if an $\alpha_i$ is
+$\sigma_i$ (for $1 \leq i \leq n$). Failure occurs if an $\alpha_i$ is
 not a type variable.
 
 The polymorphic \ML{} infix function {\small\verb+|->+} is used to
@@ -1873,7 +1873,7 @@ \subsubsection{Constant definitions}
 \index{definitions, adding to HOL logic@definitions, adding to \HOL{} logic}
 of the current theory. The name associated with the definition in
 this theory is $name$.
-Failure if:
+Failure occurs if:
 \begin{myenumerate}
 \item $t$ contains free variables that are not in any of
 the variable structures $v_1$, $\dots$, $v_n$ (this is equivalent