1.1 --- a/doc-src/Ref/classical.tex	Mon Jan 12 17:48:55 1998 +0100
     1.2 +++ b/doc-src/Ref/classical.tex	Mon Jan 12 17:49:12 1998 +0100
     1.3 @@ -558,12 +558,22 @@
     1.4  \end{ttdescription}
     1.5  
     1.6  \subsection{The current claset}\label{sec:current-claset}
     1.7 -Some logics (\FOL, {\HOL} and \ZF) support the concept of a current
     1.8 -claset\index{claset!current}.  This is a default set of classical rules.  The
     1.9 -underlying idea is quite similar to that of a current simpset described in
    1.10 -\S\ref{sec:simp-for-dummies}; please read that section, including its
    1.11 -warnings.  Just like simpsets, clasets can be associated with theories.  The
    1.12 -tactics
    1.13 +
    1.14 +Each theory is equipped with an implicit \emph{current
    1.15 +  claset}\index{claset!current}.  This is a default set of classical
    1.16 +rules.  The underlying idea is quite similar to that of a current
    1.17 +simpset described in \S\ref{sec:simp-for-dummies}; please read that
    1.18 +section, including its warnings.  The implicit claset can be accessed
    1.19 +as follows:
    1.20 +\begin{ttbox}
    1.21 +claset        : unit -> claset
    1.22 +claset_ref    : unit -> claset ref
    1.23 +claset_of     : theory -> claset
    1.24 +claset_ref_of : theory -> claset ref
    1.25 +print_claset  : theory -> unit
    1.26 +\end{ttbox}
    1.27 +
    1.28 +The tactics
    1.29  \begin{ttbox}
    1.30  Blast_tac        : int -> tactic
    1.31  Auto_tac         :        tactic
    1.32 @@ -584,10 +594,10 @@
    1.33  \indexbold{*Step_tac}
    1.34  make use of the current claset.  For example, \texttt{Blast_tac} is defined as 
    1.35  \begin{ttbox}
    1.36 -fun Blast_tac i st = blast_tac (!claset) i st;
    1.37 +fun Blast_tac i st = blast_tac (claset()) i st;
    1.38  \end{ttbox}
    1.39 -and gets the current claset, \ttindex{!claset}, only after it is applied to a
    1.40 -proof state.  The functions
    1.41 +and gets the current claset, only after it is applied to a proof
    1.42 +state.  The functions
    1.43  \begin{ttbox}
    1.44  AddSIs, AddSEs, AddSDs, AddIs, AddEs, AddDs: thm list -> unit
    1.45  \end{ttbox}