diff -r 24e156db414c -r 58db56278478 doc-src/IsarImplementation/Thy/document/Logic.tex
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex	Mon Mar 16 19:40:03 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex	Mon Mar 16 23:36:55 2009 +0100
@@ -821,12 +821,12 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexdef{}{ML}{MetaSimplifier.norm\_hhf}\verb|MetaSimplifier.norm_hhf: thm -> thm| \\
+  \indexdef{}{ML}{Simplifier.norm\_hhf}\verb|Simplifier.norm_hhf: thm -> thm| \\
   \end{mldecls}
 
   \begin{description}
 
-  \item \verb|MetaSimplifier.norm_hhf|~\isa{thm} normalizes the given
+  \item \verb|Simplifier.norm_hhf|~\isa{thm} normalizes the given
   theorem according to the canonical form specified above.  This is
   occasionally helpful to repair some low-level tools that do not
   handle Hereditary Harrop Formulae properly.