1.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Wed Feb 15 22:44:31 2012 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Wed Feb 15 23:19:30 2012 +0100
     1.3 @@ -155,7 +155,7 @@
     1.4        val (v, _) = dest_Free (term_of cv)
     1.5        val u_th = introduce_combinators_in_cterm cta
     1.6        val cu = Thm.rhs_of u_th
     1.7 -      val comb_eq = abstract (Thm.cabs cv cu)
     1.8 +      val comb_eq = abstract (Thm.lambda cv cu)
     1.9      in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
    1.10    | _ $ _ =>
    1.11      let val (ct1, ct2) = Thm.dest_comb ct in
    1.12 @@ -205,10 +205,10 @@
    1.13        | _ => raise TERM ("old_skolem_theorem_from_def: expected \"Eps\"",
    1.14                           [hilbert])
    1.15      val cex = cterm_of thy (HOLogic.exists_const T)
    1.16 -    val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs)
    1.17 +    val ex_tm = Thm.apply cTrueprop (Thm.apply cex cabs)
    1.18      val conc =
    1.19        Drule.list_comb (rhs, frees)
    1.20 -      |> Drule.beta_conv cabs |> Thm.capply cTrueprop
    1.21 +      |> Drule.beta_conv cabs |> Thm.apply cTrueprop
    1.22      fun tacf [prem] =
    1.23        rewrite_goals_tac skolem_def_raw
    1.24        THEN rtac ((prem |> rewrite_rule skolem_def_raw)