1.1 --- a/doc-src/Nitpick/nitpick.tex	Tue Oct 27 12:16:26 2009 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Tue Oct 27 14:40:24 2009 +0100
     1.3 @@ -2381,7 +2381,7 @@
     1.4  (``genuine'', ``likely\_genuine'', ``potential'', ``none'', or ``unknown''). The
     1.5  \textit{params} type is a large record that lets you set Nitpick's options. The
     1.6  current default options can be retrieved by calling the following function
     1.7 -defined in the \textit{NitpickIsar} structure:
     1.8 +defined in the \textit{Nitpick\_Isar} structure:
     1.9  
    1.10  \prew
    1.11  $\textbf{val}\,~\textit{default\_params} :\,
    1.12 @@ -2392,7 +2392,7 @@
    1.13  put into a \textit{params} record. Here is an example:
    1.14  
    1.15  \prew
    1.16 -$\textbf{val}\,~\textit{params} = \textit{NitpickIsar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\
    1.17 +$\textbf{val}\,~\textit{params} = \textit{Nitpick\_Isar.default\_params}~\textit{thy}~[(\textrm{``}\textrm{timeout}\textrm{''},\, \textrm{``}\textrm{none}\textrm{''})]$ \\
    1.18  $\textbf{val}\,~(\textit{outcome},\, \textit{state}') = \textit{Nitpick.pick\_nits\_in\_subgoal}~\begin{aligned}[t]
    1.19  & \textit{state}~\textit{params}~\textit{false} \\[-2pt]
    1.20  & \textit{subgoal}\end{aligned}$