doc-src/Logics/HOL.tex

--- a/doc-src/Logics/HOL.tex	Wed Apr 14 15:58:01 1999 +0200
+++ b/doc-src/Logics/HOL.tex	Wed Apr 14 18:55:29 1999 +0200
@@ -2971,9 +2971,8 @@
 {\out No subgoals!}
 \end{ttbox}
 If you run this example interactively, make sure your current theory contains
-theory \texttt{Set}, for example by executing
-\ttindex{set_current_thy}~{\tt"Set"}.  Otherwise the default claset may not
-contain the rules for set theory.
+theory \texttt{Set}, for example by executing \ttindex{context}~{\tt Set.thy}.
+Otherwise the default claset may not contain the rules for set theory.
 \index{higher-order logic|)}
 
 %%% Local Variables: