src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML
changeset 39720 0b93a954da4f
parent 39494 bf7dd4902321
child 39886 8a9f0c97d550
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Mon Sep 27 09:17:24 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_translate.ML	Mon Sep 27 10:44:08 2010 +0200
     1.3 @@ -94,7 +94,7 @@
     1.4                      (0 upto length Ts - 1 ~~ Ts))
     1.5  
     1.6  (* Removes the lambdas from an equation of the form "t = (%x. u)".
     1.7 -   (Cf. "extensionalize_theorem" in "Clausifier".) *)
     1.8 +   (Cf. "extensionalize_theorem" in "Meson_Clausifier".) *)
     1.9  fun extensionalize_term t =
    1.10    let
    1.11      fun aux j (@{const Trueprop} $ t') = @{const Trueprop} $ aux j t'
    1.12 @@ -141,7 +141,7 @@
    1.13                     t |> conceal_bounds Ts
    1.14                       |> Envir.eta_contract
    1.15                       |> cterm_of thy
    1.16 -                     |> Clausifier.introduce_combinators_in_cterm
    1.17 +                     |> Meson_Clausifier.introduce_combinators_in_cterm
    1.18                       |> prop_of |> Logic.dest_equals |> snd
    1.19                       |> reveal_bounds Ts
    1.20          val (t, ctxt') = Variable.import_terms true [t] ctxt |>> the_single