--- a/doc-src/Ref/simp.tex Mon Aug 28 13:50:24 2000 +0200
+++ b/doc-src/Ref/simp.tex Mon Aug 28 13:52:38 2000 +0200
@@ -489,8 +489,8 @@
\section{A sample instantiation}
-Here is the instantiation of {\tt SIMP_DATA} for {\FOL}. The code for {\tt
-mk_rew_rules} is not shown; see the file {\tt FOL/simpdata.ML}.
+Here is the instantiation of {\tt SIMP_DATA} for FOL. The code for {\tt
+ mk_rew_rules} is not shown; see the file {\tt FOL/simpdata.ML}.
\begin{ttbox}
structure FOL_SimpData : SIMP_DATA =
struct