--- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Sep 29 23:26:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML Wed Sep 29 23:30:10 2010 +0200
@@ -94,7 +94,7 @@
(0 upto length Ts - 1 ~~ Ts))
(* Removes the lambdas from an equation of the form "t = (%x. u)".
- (Cf. "extensionalize_theorem" in "Meson_Clausifier".) *)
+ (Cf. "extensionalize_theorem" in "Meson_Clausify".) *)
fun extensionalize_term t =
let
fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
@@ -141,7 +141,7 @@
t |> conceal_bounds Ts
|> Envir.eta_contract
|> cterm_of thy
- |> Meson_Clausifier.introduce_combinators_in_cterm
+ |> Meson_Clausify.introduce_combinators_in_cterm
|> prop_of |> Logic.dest_equals |> snd
|> reveal_bounds Ts
val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single