src/HOL/Tools/groebner.ML

     (refute_disj rfn (Thm.dest_arg tm), 2,
       Drule.compose_single (refute_disj rfn (Thm.dest_arg1 tm), 2, disjE))
   | _ => rfn tm ;
 
 val notnotD = @{thm notnotD};
-fun mk_binop ct x y = Thm.capply (Thm.capply ct x) y
+fun mk_binop ct x y = Thm.apply (Thm.apply ct x) y
 
 fun is_neg t =
     case term_of t of
       (Const(@{const_name Not},_)$p) => true
     | _  => false;

 val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
 
 val cTrp = @{cterm "Trueprop"};
 val cConj = @{cterm HOL.conj};
 val (cNot,false_tm) = (@{cterm "Not"}, @{cterm "False"});
-val assume_Trueprop = Thm.capply cTrp #> Thm.assume;
+val assume_Trueprop = Thm.apply cTrp #> Thm.assume;
 val list_mk_conj = list_mk_binop cConj;
 val conjs = list_dest_binop cConj;
-val mk_neg = Thm.capply cNot;
+val mk_neg = Thm.apply cNot;
 
 fun striplist dest =
  let
   fun h acc x = case try dest x of
     SOME (a,b) => h (h acc b) a
   | NONE => x::acc
  in h [] end;
-fun list_mk_binop b = foldr1 (fn (s,t) => Thm.capply (Thm.capply b s) t);
+fun list_mk_binop b = foldr1 (fn (s,t) => Thm.apply (Thm.apply b s) t);
 
 val eq_commute = mk_meta_eq @{thm eq_commute};
 
 fun sym_conv eq =
  let val (l,r) = Thm.dest_binop eq

   @{term HOL.conj}$_$_ => (Thm.dest_arg1 ct)::(conjuncts (Thm.dest_arg ct))
 | _ => [ct];
 
 fun fold1 f = foldr1 (uncurry f);
 
-val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm HOL.conj} c) c') ;
+val list_conj = fold1 (fn c => fn c' => Thm.apply (Thm.apply @{cterm HOL.conj} c) c') ;
 
 fun mk_conj_tab th =
  let fun h acc th =
    case prop_of th of
    @{term "Trueprop"}$(@{term HOL.conj}$p$q) =>

  | c::cs => conjI OF [prove_conj tab [c], prove_conj tab cs];
 
 fun conj_ac_rule eq =
  let
   val (l,r) = Thm.dest_equals eq
-  val ctabl = mk_conj_tab (Thm.assume (Thm.capply @{cterm Trueprop} l))
-  val ctabr = mk_conj_tab (Thm.assume (Thm.capply @{cterm Trueprop} r))
+  val ctabl = mk_conj_tab (Thm.assume (Thm.apply @{cterm Trueprop} l))
+  val ctabr = mk_conj_tab (Thm.assume (Thm.apply @{cterm Trueprop} r))
   fun tabl c = the (Termtab.lookup ctabl (term_of c))
   fun tabr c = the (Termtab.lookup ctabr (term_of c))
   val thl  = prove_conj tabl (conjuncts r) |> implies_intr_hyps
   val thr  = prove_conj tabr (conjuncts l) |> implies_intr_hyps
   val eqI = instantiate' [] [SOME l, SOME r] @{thm iffI}

  (* END FIXME.*)
 
    (* Conversion for the equivalence of existential statements where
       EX quantifiers are rearranged differently *)
  fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
- fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
+ fun mk_ex v t = Thm.apply (ext (ctyp_of_term v)) (Thm.lambda v t)
 
 fun choose v th th' = case concl_of th of
   @{term Trueprop} $ (Const(@{const_name Ex},_)$_) =>
    let
     val p = (funpow 2 Thm.dest_arg o cprop_of) th
     val T = (hd o Thm.dest_ctyp o ctyp_of_term) p
     val th0 = Conv.fconv_rule (Thm.beta_conversion true)
         (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE)
     val pv = (Thm.rhs_of o Thm.beta_conversion true)
-          (Thm.capply @{cterm Trueprop} (Thm.capply p v))
+          (Thm.apply @{cterm Trueprop} (Thm.apply p v))
     val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
    in Thm.implies_elim (Thm.implies_elim th0 th) th1  end
 | _ => error ""  (* FIXME ? *)
 
 fun simple_choose v th =
-   choose v (Thm.assume ((Thm.capply @{cterm Trueprop} o mk_ex v)
+   choose v (Thm.assume ((Thm.apply @{cterm Trueprop} o mk_ex v)
     ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
 
 
  fun mkexi v th =
   let
-   val p = Thm.cabs v (Thm.dest_arg (Thm.cprop_of th))
+   val p = Thm.lambda v (Thm.dest_arg (Thm.cprop_of th))
   in Thm.implies_elim
     (Conv.fconv_rule (Thm.beta_conversion true)
       (instantiate' [SOME (ctyp_of_term v)] [SOME p, SOME v] @{thm exI}))
       th
   end
  fun ex_eq_conv t =
   let
   val (p0,q0) = Thm.dest_binop t
   val (vs',P) = strip_exists p0
   val (vs,_) = strip_exists q0
-   val th = Thm.assume (Thm.capply @{cterm Trueprop} P)
+   val th = Thm.assume (Thm.apply @{cterm Trueprop} P)
    val th1 = implies_intr_hyps (fold simple_choose vs' (fold mkexi vs th))
    val th2 = implies_intr_hyps (fold simple_choose vs (fold mkexi vs' th))
    val p = (Thm.dest_arg o Thm.dest_arg1 o cprop_of) th1
    val q = (Thm.dest_arg o Thm.dest_arg o cprop_of) th1
   in Thm.implies_elim (Thm.implies_elim (instantiate' [] [SOME p, SOME q] iffI) th1) th2

 
  fun getname v = case term_of v of
   Free(s,_) => s
  | Var ((s,_),_) => s
  | _ => "x"
- fun mk_eq s t = Thm.capply (Thm.capply @{cterm "op == :: bool => _"} s) t
- fun mkeq s t = Thm.capply @{cterm Trueprop} (Thm.capply (Thm.capply @{cterm "op = :: bool => _"} s) t)
+ fun mk_eq s t = Thm.apply (Thm.apply @{cterm "op == :: bool => _"} s) t
+ fun mkeq s t = Thm.apply @{cterm Trueprop} (Thm.apply (Thm.apply @{cterm "op = :: bool => _"} s) t)
  fun mk_exists v th = Drule.arg_cong_rule (ext (ctyp_of_term v))
    (Thm.abstract_rule (getname v) v th)
  val simp_ex_conv =
      Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms(39)})
 
 fun frees t = Thm.add_cterm_frees t [];
 fun free_in v t = member op aconvc (frees t) v;
 
 val vsubst = let
  fun vsubst (t,v) tm =
-   (Thm.rhs_of o Thm.beta_conversion false) (Thm.capply (Thm.cabs v tm) t)
+   (Thm.rhs_of o Thm.beta_conversion false) (Thm.apply (Thm.lambda v tm) t)
 in fold vsubst end;
 
 
 (** main **)
 

     let val (l,r) = Thm.dest_comb t
     in if Term.could_unify(term_of l,term_of ring_neg_tm) then r
        else raise CTERM ("ring_dest_neg", [t])
     end
 
- val ring_mk_neg = fn tm => Thm.capply (ring_neg_tm) (tm);
+ val ring_mk_neg = fn tm => Thm.apply (ring_neg_tm) (tm);
  fun field_dest_inv t =
     let val (l,r) = Thm.dest_comb t in
         if Term.could_unify(term_of l, term_of field_inv_tm) then r
         else raise CTERM ("field_dest_inv", [t])
     end

       val th2 =
         Conv.fconv_rule
           ((Conv.arg_conv #> Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) th1
       val conc = th2 |> concl |> Thm.dest_arg
       val (l,r) = conc |> dest_eq
-    in Thm.implies_intr (Thm.capply cTrp tm)
+    in Thm.implies_intr (Thm.apply cTrp tm)
                     (Thm.equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th2))
                            (Thm.reflexive l |> mk_object_eq))
     end
    else
    let

     val  herts_pos = map (fn (i,p) => (i,holify_polynomial vars p)) cert_pos
     val  herts_neg = map (fn (i,p) => (i,holify_polynomial vars p)) cert_neg
     fun thm_fn pols =
         if null pols then Thm.reflexive(mk_const rat_0) else
         end_itlist mk_add
-            (map (fn (i,p) => Drule.arg_cong_rule (Thm.capply ring_mul_tm p)
+            (map (fn (i,p) => Drule.arg_cong_rule (Thm.apply ring_mul_tm p)
               (nth eths i |> mk_meta_eq)) pols)
     val th1 = thm_fn herts_pos
     val th2 = thm_fn herts_neg
     val th3 = HOLogic.conj_intr(mk_add (Thm.symmetric th1) th2 |> mk_object_eq) noteqth
     val th4 =
       Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv o Conv.binop_conv) ring_normalize_conv)
         (neq_rule l th3)
     val (l,r) = dest_eq(Thm.dest_arg(concl th4))
-   in Thm.implies_intr (Thm.capply cTrp tm)
+   in Thm.implies_intr (Thm.apply cTrp tm)
                         (Thm.equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th4))
                    (Thm.reflexive l |> mk_object_eq))
    end
   end) handle ERROR _ => raise CTERM ("Groebner-refute: unable to refute",[tm]))
 
 fun ring tm =
  let
   fun mk_forall x p =
-    Thm.capply
+    Thm.apply
       (Drule.cterm_rule (instantiate' [SOME (ctyp_of_term x)] [])
-        @{cpat "All:: (?'a => bool) => _"}) (Thm.cabs x p)
+        @{cpat "All:: (?'a => bool) => _"}) (Thm.lambda x p)
   val avs = Thm.add_cterm_frees tm []
   val P' = fold mk_forall avs tm
   val th1 = initial_conv(mk_neg P')
   val (evs,bod) = strip_exists(concl th1) in
    if is_forall bod then raise CTERM("ring: non-universal formula",[tm])

   val (cmons,vmons) =
     List.partition (fn m => null (inter (op aconvc) vars (frees m)))
                    (striplist ring_dest_add tm)
   val cofactors = map (fn v => find_multipliers v vmons) vars
   val cnc = if null cmons then zero_tm
-             else Thm.capply ring_neg_tm
+             else Thm.apply ring_neg_tm
                     (list_mk_binop ring_add_tm cmons)
   in (cofactors,cnc)
   end;
 
 fun isolate_variables evs ps eq =