--- a/doc-src/IsarImplementation/Thy/Logic.thy Mon Mar 16 19:40:03 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Logic.thy Mon Mar 16 23:36:55 2009 +0100
@@ -807,12 +807,12 @@
text %mlref {*
\begin{mldecls}
- @{index_ML MetaSimplifier.norm_hhf: "thm -> thm"} \\
+ @{index_ML Simplifier.norm_hhf: "thm -> thm"} \\
\end{mldecls}
\begin{description}
- \item @{ML MetaSimplifier.norm_hhf}~@{text thm} normalizes the given
+ \item @{ML Simplifier.norm_hhf}~@{text 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.