--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Sep 29 23:26:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Wed Sep 29 23:30:10 2010 +0200
@@ -98,7 +98,7 @@
(* Converts an elim-rule into an equivalent theorem that does not have the
predicate variable. Leaves other theorems unchanged. We simply instantiate
the conclusion variable to False. (Cf. "transform_elim_theorem" in
- "Meson_Clausifier".) *)
+ "Meson_Clausify".) *)
fun transform_elim_term t =
case Logic.strip_imp_concl t of
@{const Trueprop} $ Var (z, @{typ bool}) =>