renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
authorwenzelm
Wed Feb 15 23:19:30 2012 +0100 (2012-02-15)
changeset 4649789ccf66aa73d
parent 46496 b8920f3fd259
child 46498 2754784e9153
renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
NEWS
doc-src/IsarImplementation/Thy/Logic.thy
doc-src/IsarImplementation/Thy/document/Logic.tex
src/HOL/Boogie/Tools/boogie_vcs.ML
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/Decision_Procs/ferrante_rackoff.ML
src/HOL/Decision_Procs/langford.ML
src/HOL/HOL.thy
src/HOL/Library/Efficient_Nat.thy
src/HOL/Library/Sum_of_Squares/sum_of_squares.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/Multivariate_Analysis/normarith.ML
src/HOL/Tools/Meson/meson_clausify.ML
src/HOL/Tools/Qelim/cooper.ML
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/SMT/smt_real.ML
src/HOL/Tools/SMT/smt_solver.ML
src/HOL/Tools/SMT/smt_utils.ML
src/HOL/Tools/SMT/z3_interface.ML
src/HOL/Tools/SMT/z3_proof_literals.ML
src/HOL/Tools/SMT/z3_proof_methods.ML
src/HOL/Tools/SMT/z3_proof_parser.ML
src/HOL/Tools/SMT/z3_proof_reconstruction.ML
src/HOL/Tools/SMT/z3_proof_tools.ML
src/HOL/Tools/TFL/dcterm.ML
src/HOL/Tools/groebner.ML
src/HOL/Tools/numeral.ML
src/HOL/Tools/numeral_simprocs.ML
src/HOL/Tools/semiring_normalizer.ML
src/HOL/Tools/transfer.ML
src/Pure/conjunction.ML
src/Pure/drule.ML
src/Pure/more_thm.ML
src/Pure/thm.ML
src/Pure/variable.ML
src/Tools/Code/code_preproc.ML
     1.1 --- a/NEWS	Wed Feb 15 22:44:31 2012 +0100
     1.2 +++ b/NEWS	Wed Feb 15 23:19:30 2012 +0100
     1.3 @@ -332,6 +332,9 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in
     1.8 +conformance with similar operations in structure Term and Logic.
     1.9 +
    1.10  * Antiquotation @{attributes [...]} embeds attribute source
    1.11  representation into the ML text, which is particularly useful with
    1.12  declarations like Local_Theory.note.
     2.1 --- a/doc-src/IsarImplementation/Thy/Logic.thy	Wed Feb 15 22:44:31 2012 +0100
     2.2 +++ b/doc-src/IsarImplementation/Thy/Logic.thy	Wed Feb 15 23:19:30 2012 +0100
     2.3 @@ -641,8 +641,8 @@
     2.4    @{index_ML_type cterm} \\
     2.5    @{index_ML Thm.ctyp_of: "theory -> typ -> ctyp"} \\
     2.6    @{index_ML Thm.cterm_of: "theory -> term -> cterm"} \\
     2.7 -  @{index_ML Thm.capply: "cterm -> cterm -> cterm"} \\
     2.8 -  @{index_ML Thm.cabs: "cterm -> cterm -> cterm"} \\
     2.9 +  @{index_ML Thm.apply: "cterm -> cterm -> cterm"} \\
    2.10 +  @{index_ML Thm.lambda: "cterm -> cterm -> cterm"} \\
    2.11    @{index_ML Thm.all: "cterm -> cterm -> cterm"} \\
    2.12    @{index_ML Drule.mk_implies: "cterm * cterm -> cterm"} \\
    2.13    \end{mldecls}
    2.14 @@ -697,7 +697,7 @@
    2.15    Full re-certification is relatively slow and should be avoided in
    2.16    tight reasoning loops.
    2.17  
    2.18 -  \item @{ML Thm.capply}, @{ML Thm.cabs}, @{ML Thm.all}, @{ML
    2.19 +  \item @{ML Thm.apply}, @{ML Thm.lambda}, @{ML Thm.all}, @{ML
    2.20    Drule.mk_implies} etc.\ compose certified terms (or propositions)
    2.21    incrementally.  This is equivalent to @{ML Thm.cterm_of} after
    2.22    unchecked @{ML_op "$"}, @{ML lambda}, @{ML Logic.all}, @{ML
     3.1 --- a/doc-src/IsarImplementation/Thy/document/Logic.tex	Wed Feb 15 22:44:31 2012 +0100
     3.2 +++ b/doc-src/IsarImplementation/Thy/document/Logic.tex	Wed Feb 15 23:19:30 2012 +0100
     3.3 @@ -712,8 +712,8 @@
     3.4    \indexdef{}{ML type}{cterm}\verb|type cterm| \\
     3.5    \indexdef{}{ML}{Thm.ctyp\_of}\verb|Thm.ctyp_of: theory -> typ -> ctyp| \\
     3.6    \indexdef{}{ML}{Thm.cterm\_of}\verb|Thm.cterm_of: theory -> term -> cterm| \\
     3.7 -  \indexdef{}{ML}{Thm.capply}\verb|Thm.capply: cterm -> cterm -> cterm| \\
     3.8 -  \indexdef{}{ML}{Thm.cabs}\verb|Thm.cabs: cterm -> cterm -> cterm| \\
     3.9 +  \indexdef{}{ML}{Thm.apply}\verb|Thm.apply: cterm -> cterm -> cterm| \\
    3.10 +  \indexdef{}{ML}{Thm.lambda}\verb|Thm.lambda: cterm -> cterm -> cterm| \\
    3.11    \indexdef{}{ML}{Thm.all}\verb|Thm.all: cterm -> cterm -> cterm| \\
    3.12    \indexdef{}{ML}{Drule.mk\_implies}\verb|Drule.mk_implies: cterm * cterm -> cterm| \\
    3.13    \end{mldecls}
    3.14 @@ -767,7 +767,7 @@
    3.15    Full re-certification is relatively slow and should be avoided in
    3.16    tight reasoning loops.
    3.17  
    3.18 -  \item \verb|Thm.capply|, \verb|Thm.cabs|, \verb|Thm.all|, \verb|Drule.mk_implies| etc.\ compose certified terms (or propositions)
    3.19 +  \item \verb|Thm.apply|, \verb|Thm.lambda|, \verb|Thm.all|, \verb|Drule.mk_implies| etc.\ compose certified terms (or propositions)
    3.20    incrementally.  This is equivalent to \verb|Thm.cterm_of| after
    3.21    unchecked \verb|$|, \verb|lambda|, \verb|Logic.all|, \verb|Logic.mk_implies| etc., but there can be a big difference in
    3.22    performance when large existing entities are composed by a few extra
     4.1 --- a/src/HOL/Boogie/Tools/boogie_vcs.ML	Wed Feb 15 22:44:31 2012 +0100
     4.2 +++ b/src/HOL/Boogie/Tools/boogie_vcs.ML	Wed Feb 15 23:19:30 2012 +0100
     4.3 @@ -220,7 +220,7 @@
     4.4  
     4.5  fun join (Assume (_, pv), pthm) (Assume (t, v), thm) =
     4.6        let
     4.7 -        val mk_prop = Thm.capply @{cterm Trueprop}
     4.8 +        val mk_prop = Thm.apply @{cterm Trueprop}
     4.9          val ct = Thm.cprop_of thm |> Thm.dest_arg |> Thm.dest_arg1 |> mk_prop
    4.10          val th = Thm.assume ct
    4.11          val (v', thm') = join (pv, imp_elim th pthm) (v, imp_elim th thm)
     5.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Feb 15 22:44:31 2012 +0100
     5.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Wed Feb 15 23:19:30 2012 +0100
     5.3 @@ -660,8 +660,8 @@
     5.4  fun mk_frac phi cT x =
     5.5   let val (a, b) = Rat.quotient_of_rat x
     5.6   in if b = 1 then Numeral.mk_cnumber cT a
     5.7 -    else Thm.capply
     5.8 -         (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
     5.9 +    else Thm.apply
    5.10 +         (Thm.apply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
    5.11                       (Numeral.mk_cnumber cT a))
    5.12           (Numeral.mk_cnumber cT b)
    5.13   end
    5.14 @@ -690,9 +690,9 @@
    5.15          val cz = Thm.dest_arg ct
    5.16          val neg = cr </ Rat.zero
    5.17          val cthp = Simplifier.rewrite (simpset_of ctxt)
    5.18 -               (Thm.capply @{cterm "Trueprop"}
    5.19 -                  (if neg then Thm.capply (Thm.capply clt c) cz
    5.20 -                    else Thm.capply (Thm.capply clt cz) c))
    5.21 +               (Thm.apply @{cterm "Trueprop"}
    5.22 +                  (if neg then Thm.apply (Thm.apply clt c) cz
    5.23 +                    else Thm.apply (Thm.apply clt cz) c))
    5.24          val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    5.25          val th = Thm.implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x,t])
    5.26               (if neg then @{thm neg_prod_sum_lt} else @{thm pos_prod_sum_lt})) cth
    5.27 @@ -713,9 +713,9 @@
    5.28          val cz = Thm.dest_arg ct
    5.29          val neg = cr </ Rat.zero
    5.30          val cthp = Simplifier.rewrite (simpset_of ctxt)
    5.31 -               (Thm.capply @{cterm "Trueprop"}
    5.32 -                  (if neg then Thm.capply (Thm.capply clt c) cz
    5.33 -                    else Thm.capply (Thm.capply clt cz) c))
    5.34 +               (Thm.apply @{cterm "Trueprop"}
    5.35 +                  (if neg then Thm.apply (Thm.apply clt c) cz
    5.36 +                    else Thm.apply (Thm.apply clt cz) c))
    5.37          val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    5.38          val th = Thm.implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x])
    5.39               (if neg then @{thm neg_prod_lt} else @{thm pos_prod_lt})) cth
    5.40 @@ -734,9 +734,9 @@
    5.41          val cz = Thm.dest_arg ct
    5.42          val neg = cr </ Rat.zero
    5.43          val cthp = Simplifier.rewrite (simpset_of ctxt)
    5.44 -               (Thm.capply @{cterm "Trueprop"}
    5.45 -                  (if neg then Thm.capply (Thm.capply clt c) cz
    5.46 -                    else Thm.capply (Thm.capply clt cz) c))
    5.47 +               (Thm.apply @{cterm "Trueprop"}
    5.48 +                  (if neg then Thm.apply (Thm.apply clt c) cz
    5.49 +                    else Thm.apply (Thm.apply clt cz) c))
    5.50          val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    5.51          val th = Thm.implies_elim (instantiate' [SOME T] (map SOME [c,x,t])
    5.52               (if neg then @{thm neg_prod_sum_le} else @{thm pos_prod_sum_le})) cth
    5.53 @@ -758,9 +758,9 @@
    5.54          val cz = Thm.dest_arg ct
    5.55          val neg = cr </ Rat.zero
    5.56          val cthp = Simplifier.rewrite (simpset_of ctxt)
    5.57 -               (Thm.capply @{cterm "Trueprop"}
    5.58 -                  (if neg then Thm.capply (Thm.capply clt c) cz
    5.59 -                    else Thm.capply (Thm.capply clt cz) c))
    5.60 +               (Thm.apply @{cterm "Trueprop"}
    5.61 +                  (if neg then Thm.apply (Thm.apply clt c) cz
    5.62 +                    else Thm.apply (Thm.apply clt cz) c))
    5.63          val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    5.64          val th = Thm.implies_elim (instantiate' [SOME (ctyp_of_term x)] (map SOME [c,x])
    5.65               (if neg then @{thm neg_prod_le} else @{thm pos_prod_le})) cth
    5.66 @@ -777,8 +777,8 @@
    5.67          val ceq = Thm.dest_fun2 ct
    5.68          val cz = Thm.dest_arg ct
    5.69          val cthp = Simplifier.rewrite (simpset_of ctxt)
    5.70 -            (Thm.capply @{cterm "Trueprop"}
    5.71 -             (Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz)))
    5.72 +            (Thm.apply @{cterm "Trueprop"}
    5.73 +             (Thm.apply @{cterm "Not"} (Thm.apply (Thm.apply ceq c) cz)))
    5.74          val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    5.75          val th = Thm.implies_elim
    5.76                   (instantiate' [SOME T] (map SOME [c,x,t]) @{thm nz_prod_sum_eq}) cth
    5.77 @@ -799,8 +799,8 @@
    5.78          val ceq = Thm.dest_fun2 ct
    5.79          val cz = Thm.dest_arg ct
    5.80          val cthp = Simplifier.rewrite (simpset_of ctxt)
    5.81 -            (Thm.capply @{cterm "Trueprop"}
    5.82 -             (Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz)))
    5.83 +            (Thm.apply @{cterm "Trueprop"}
    5.84 +             (Thm.apply @{cterm "Not"} (Thm.apply (Thm.apply ceq c) cz)))
    5.85          val cth = Thm.equal_elim (Thm.symmetric cthp) TrueI
    5.86          val rth = Thm.implies_elim
    5.87                   (instantiate' [SOME T] (map SOME [c,x]) @{thm nz_prod_eq}) cth
     6.1 --- a/src/HOL/Decision_Procs/ferrante_rackoff.ML	Wed Feb 15 22:44:31 2012 +0100
     6.2 +++ b/src/HOL/Decision_Procs/ferrante_rackoff.ML	Wed Feb 15 23:19:30 2012 +0100
     6.3 @@ -125,12 +125,12 @@
     6.4         Const(@{const_name HOL.conj},_)$_$_ =>
     6.5          let val (p,q) = Thm.dest_binop fm
     6.6          in ([p,q], myfwd (minf_conj,pinf_conj, nmi_conj, npi_conj,ld_conj)
     6.7 -                         (Thm.cabs x p) (Thm.cabs x q))
     6.8 +                         (Thm.lambda x p) (Thm.lambda x q))
     6.9          end
    6.10       | Const(@{const_name HOL.disj},_)$_$_ =>
    6.11          let val (p,q) = Thm.dest_binop fm
    6.12          in ([p,q],myfwd (minf_disj, pinf_disj, nmi_disj, npi_disj,ld_disj)
    6.13 -                         (Thm.cabs x p) (Thm.cabs x q))
    6.14 +                         (Thm.lambda x p) (Thm.lambda x q))
    6.15          end
    6.16       | _ =>
    6.17          (let val c = wi x fm
     7.1 --- a/src/HOL/Decision_Procs/langford.ML	Wed Feb 15 22:44:31 2012 +0100
     7.2 +++ b/src/HOL/Decision_Procs/langford.ML	Wed Feb 15 23:19:30 2012 +0100
     7.3 @@ -82,7 +82,7 @@
     7.4  
     7.5  fun fold1 f = foldr1 (uncurry f);
     7.6  
     7.7 -val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm HOL.conj} c) c') ;
     7.8 +val list_conj = fold1 (fn c => fn c' => Thm.apply (Thm.apply @{cterm HOL.conj} c) c') ;
     7.9  
    7.10  fun mk_conj_tab th = 
    7.11   let fun h acc th = 
    7.12 @@ -128,7 +128,7 @@
    7.13     let 
    7.14      val e = Thm.dest_fun ct
    7.15      val (x,p) = Thm.dest_abs (SOME xn) (Thm.dest_arg ct)
    7.16 -    val Pp = Thm.capply @{cterm "Trueprop"} p 
    7.17 +    val Pp = Thm.apply @{cterm "Trueprop"} p 
    7.18      val (eqs,neqs) = List.partition (is_eqx x) (all_conjuncts p)
    7.19     in case eqs of
    7.20        [] => 
    7.21 @@ -137,14 +137,14 @@
    7.22           in case ndx of [] => NONE
    7.23                        | _ =>
    7.24              conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp 
    7.25 -                 (Thm.capply @{cterm Trueprop} (list_conj (ndx @dx))))
    7.26 +                 (Thm.apply @{cterm Trueprop} (list_conj (ndx @dx))))
    7.27             |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e 
    7.28             |> Conv.fconv_rule (Conv.arg_conv 
    7.29                     (Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms ex_simps})))
    7.30             |> SOME
    7.31            end
    7.32      | _ => conj_aci_rule (Thm.mk_binop @{cterm "op == :: prop => _"} Pp 
    7.33 -                 (Thm.capply @{cterm Trueprop} (list_conj (eqs@neqs))))
    7.34 +                 (Thm.apply @{cterm Trueprop} (list_conj (eqs@neqs))))
    7.35             |> Thm.abstract_rule xn x |> Drule.arg_cong_rule e 
    7.36             |> Conv.fconv_rule (Conv.arg_conv 
    7.37                     (Simplifier.rewrite (HOL_basic_ss addsimps @{thms simp_thms ex_simps})))
    7.38 @@ -209,7 +209,7 @@
    7.39  fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st =>
    7.40   let 
    7.41     fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
    7.42 -   fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
    7.43 +   fun gen x t = Thm.apply (all (ctyp_of_term x)) (Thm.lambda x t)
    7.44     val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
    7.45     val p' = fold_rev gen ts p
    7.46   in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
     8.1 --- a/src/HOL/HOL.thy	Wed Feb 15 22:44:31 2012 +0100
     8.2 +++ b/src/HOL/HOL.thy	Wed Feb 15 23:19:30 2012 +0100
     8.3 @@ -1271,7 +1271,7 @@
     8.4            val cx = cterm_of thy x;
     8.5            val {T = xT, ...} = rep_cterm cx;
     8.6            val cf = cterm_of thy f;
     8.7 -          val fx_g = Simplifier.rewrite ss (Thm.capply cf cx);
     8.8 +          val fx_g = Simplifier.rewrite ss (Thm.apply cf cx);
     8.9            val (_ $ _ $ g) = prop_of fx_g;
    8.10            val g' = abstract_over (x,g);
    8.11          in (if (g aconv g')
     9.1 --- a/src/HOL/Library/Efficient_Nat.thy	Wed Feb 15 22:44:31 2012 +0100
     9.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Wed Feb 15 23:19:30 2012 +0100
     9.3 @@ -124,8 +124,8 @@
     9.4        | _ $ _ =>
     9.5          let val (ct1, ct2) = Thm.dest_comb ct
     9.6          in 
     9.7 -          map (apfst (fn ct => Thm.capply ct ct2)) (find_vars ct1) @
     9.8 -          map (apfst (Thm.capply ct1)) (find_vars ct2)
     9.9 +          map (apfst (fn ct => Thm.apply ct ct2)) (find_vars ct1) @
    9.10 +          map (apfst (Thm.apply ct1)) (find_vars ct2)
    9.11          end
    9.12        | _ => []);
    9.13      val eqs = maps
    9.14 @@ -136,8 +136,8 @@
    9.15            Thm.implies_elim
    9.16             (Conv.fconv_rule (Thm.beta_conversion true)
    9.17               (Drule.instantiate'
    9.18 -               [SOME (ctyp_of_term ct)] [SOME (Thm.cabs cv ct),
    9.19 -                 SOME (Thm.cabs cv' (rhs_of th)), NONE, SOME cv']
    9.20 +               [SOME (ctyp_of_term ct)] [SOME (Thm.lambda cv ct),
    9.21 +                 SOME (Thm.lambda cv' (rhs_of th)), NONE, SOME cv']
    9.22                 @{thm Suc_if_eq})) (Thm.forall_intr cv' th)
    9.23        in
    9.24          case map_filter (fn th'' =>
    10.1 --- a/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Feb 15 22:44:31 2012 +0100
    10.2 +++ b/src/HOL/Library/Sum_of_Squares/sum_of_squares.ML	Wed Feb 15 23:19:30 2012 +0100
    10.3 @@ -772,7 +772,7 @@
    10.4    (* FIXME : This is very bad!!!*)
    10.5  fun subst_conv eqs t =
    10.6   let
    10.7 -  val t' = fold (Thm.cabs o Thm.lhs_of) eqs t
    10.8 +  val t' = fold (Thm.lambda o Thm.lhs_of) eqs t
    10.9   in Conv.fconv_rule (Thm.beta_conversion true) (fold (C Thm.combination) eqs (Thm.reflexive t'))
   10.10   end
   10.11  
   10.12 @@ -819,7 +819,7 @@
   10.13    fun make_substitution th =
   10.14     let
   10.15      val (c,v) = substitutable_monomial [] (Thm.dest_arg1(concl th))
   10.16 -    val th1 = Drule.arg_cong_rule (Thm.capply @{cterm "op * :: real => _"} (RealArith.cterm_of_rat (Rat.inv c))) (mk_meta_eq th)
   10.17 +    val th1 = Drule.arg_cong_rule (Thm.apply @{cterm "op * :: real => _"} (RealArith.cterm_of_rat (Rat.inv c))) (mk_meta_eq th)
   10.18      val th2 = fconv_rule (binop_conv real_poly_mul_conv) th1
   10.19     in fconv_rule (arg_conv real_poly_conv) (isolate_variable v th2)
   10.20     end
    11.1 --- a/src/HOL/Library/positivstellensatz.ML	Wed Feb 15 22:44:31 2012 +0100
    11.2 +++ b/src/HOL/Library/positivstellensatz.ML	Wed Feb 15 23:19:30 2012 +0100
    11.3 @@ -285,7 +285,7 @@
    11.4  let val (a, b) = Rat.quotient_of_rat x
    11.5  in 
    11.6   if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a
    11.7 -  else Thm.capply (Thm.capply @{cterm "op / :: real => _"} 
    11.8 +  else Thm.apply (Thm.apply @{cterm "op / :: real => _"} 
    11.9                     (Numeral.mk_cnumber @{ctyp "real"} a))
   11.10          (Numeral.mk_cnumber @{ctyp "real"} b)
   11.11  end;
   11.12 @@ -319,7 +319,7 @@
   11.13  
   11.14  (* Map back polynomials to HOL.                         *)
   11.15  
   11.16 -fun cterm_of_varpow x k = if k = 1 then x else Thm.capply (Thm.capply @{cterm "op ^ :: real => _"} x) 
   11.17 +fun cterm_of_varpow x k = if k = 1 then x else Thm.apply (Thm.apply @{cterm "op ^ :: real => _"} x) 
   11.18    (Numeral.mk_cnumber @{ctyp nat} k)
   11.19  
   11.20  fun cterm_of_monomial m = 
   11.21 @@ -328,12 +328,12 @@
   11.22    let 
   11.23     val m' = FuncUtil.dest_monomial m
   11.24     val vps = fold_rev (fn (x,k) => cons (cterm_of_varpow x k)) m' [] 
   11.25 -  in foldr1 (fn (s, t) => Thm.capply (Thm.capply @{cterm "op * :: real => _"} s) t) vps
   11.26 +  in foldr1 (fn (s, t) => Thm.apply (Thm.apply @{cterm "op * :: real => _"} s) t) vps
   11.27    end
   11.28  
   11.29  fun cterm_of_cmonomial (m,c) = if FuncUtil.Ctermfunc.is_empty m then cterm_of_rat c
   11.30      else if c = Rat.one then cterm_of_monomial m
   11.31 -    else Thm.capply (Thm.capply @{cterm "op *::real => _"} (cterm_of_rat c)) (cterm_of_monomial m);
   11.32 +    else Thm.apply (Thm.apply @{cterm "op *::real => _"} (cterm_of_rat c)) (cterm_of_monomial m);
   11.33  
   11.34  fun cterm_of_poly p = 
   11.35   if FuncUtil.Monomialfunc.is_empty p then @{cterm "0::real"} 
   11.36 @@ -341,7 +341,7 @@
   11.37    let 
   11.38     val cms = map cterm_of_cmonomial
   11.39       (sort (prod_ord FuncUtil.monomial_order (K EQUAL)) (FuncUtil.Monomialfunc.dest p))
   11.40 -  in foldr1 (fn (t1, t2) => Thm.capply(Thm.capply @{cterm "op + :: real => _"} t1) t2) cms
   11.41 +  in foldr1 (fn (t1, t2) => Thm.apply(Thm.apply @{cterm "op + :: real => _"} t1) t2) cms
   11.42    end;
   11.43  
   11.44      (* A general real arithmetic prover *)
   11.45 @@ -397,14 +397,14 @@
   11.46          Axiom_eq n => nth eqs n
   11.47        | Axiom_le n => nth les n
   11.48        | Axiom_lt n => nth lts n
   11.49 -      | Rational_eq x => eqT_elim(numeric_eq_conv(Thm.capply @{cterm Trueprop} 
   11.50 -                          (Thm.capply (Thm.capply @{cterm "op =::real => _"} (mk_numeric x)) 
   11.51 +      | Rational_eq x => eqT_elim(numeric_eq_conv(Thm.apply @{cterm Trueprop} 
   11.52 +                          (Thm.apply (Thm.apply @{cterm "op =::real => _"} (mk_numeric x)) 
   11.53                                 @{cterm "0::real"})))
   11.54 -      | Rational_le x => eqT_elim(numeric_ge_conv(Thm.capply @{cterm Trueprop} 
   11.55 -                          (Thm.capply (Thm.capply @{cterm "op <=::real => _"} 
   11.56 +      | Rational_le x => eqT_elim(numeric_ge_conv(Thm.apply @{cterm Trueprop} 
   11.57 +                          (Thm.apply (Thm.apply @{cterm "op <=::real => _"} 
   11.58                                       @{cterm "0::real"}) (mk_numeric x))))
   11.59 -      | Rational_lt x => eqT_elim(numeric_gt_conv(Thm.capply @{cterm Trueprop} 
   11.60 -                      (Thm.capply (Thm.capply @{cterm "op <::real => _"} @{cterm "0::real"})
   11.61 +      | Rational_lt x => eqT_elim(numeric_gt_conv(Thm.apply @{cterm Trueprop} 
   11.62 +                      (Thm.apply (Thm.apply @{cterm "op <::real => _"} @{cterm "0::real"})
   11.63                          (mk_numeric x))))
   11.64        | Square pt => square_rule (cterm_of_poly pt)
   11.65        | Eqmul(pt,p) => emul_rule (cterm_of_poly pt) (translate p)
   11.66 @@ -432,8 +432,8 @@
   11.67         val _ = if c aconvc (concl th2) then () else error "disj_cases : conclusions not alpha convertible"
   11.68     in Thm.implies_elim (Thm.implies_elim
   11.69            (Thm.implies_elim (instantiate' [] (map SOME [p,q,c]) @{thm disjE}) th)
   11.70 -          (Thm.implies_intr (Thm.capply @{cterm Trueprop} p) th1))
   11.71 -        (Thm.implies_intr (Thm.capply @{cterm Trueprop} q) th2)
   11.72 +          (Thm.implies_intr (Thm.apply @{cterm Trueprop} p) th1))
   11.73 +        (Thm.implies_intr (Thm.apply @{cterm Trueprop} q) th2)
   11.74     end
   11.75   fun overall cert_choice dun ths = case ths of
   11.76    [] =>
   11.77 @@ -452,8 +452,8 @@
   11.78        overall cert_choice dun (th1::th2::oths) end
   11.79      else if is_disj ct then
   11.80        let 
   11.81 -       val (th1, cert1) = overall (Left::cert_choice) dun (Thm.assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths)
   11.82 -       val (th2, cert2) = overall (Right::cert_choice) dun (Thm.assume (Thm.capply @{cterm Trueprop} (Thm.dest_arg ct))::oths)
   11.83 +       val (th1, cert1) = overall (Left::cert_choice) dun (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg1 ct))::oths)
   11.84 +       val (th2, cert2) = overall (Right::cert_choice) dun (Thm.assume (Thm.apply @{cterm Trueprop} (Thm.dest_arg ct))::oths)
   11.85        in (disj_cases th th1 th2, Branch (cert1, cert2)) end
   11.86     else overall cert_choice (th::dun) oths
   11.87    end
   11.88 @@ -469,8 +469,8 @@
   11.89      val th_x = Drule.arg_cong_rule @{cterm "uminus :: real => _"} th_p
   11.90      val th_n = fconv_rule (arg_conv poly_neg_conv) th_x
   11.91      val th' = Drule.binop_cong_rule @{cterm HOL.disj} 
   11.92 -     (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
   11.93 -     (Drule.arg_cong_rule (Thm.capply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
   11.94 +     (Drule.arg_cong_rule (Thm.apply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_p)
   11.95 +     (Drule.arg_cong_rule (Thm.apply @{cterm "op <::real=>_"} @{cterm "0::real"}) th_n)
   11.96      in Thm.transitive th th' 
   11.97    end
   11.98   fun equal_implies_1_rule PQ = 
   11.99 @@ -496,7 +496,7 @@
  11.100    val specl = fold_rev (fn x => fn th => instantiate' [] [SOME x] (th RS spec));
  11.101  
  11.102   fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
  11.103 - fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
  11.104 + fun mk_ex v t = Thm.apply (ext (ctyp_of_term v)) (Thm.lambda v t)
  11.105  
  11.106   fun choose v th th' = case concl_of th of 
  11.107     @{term Trueprop} $ (Const(@{const_name Ex},_)$_) => 
  11.108 @@ -506,13 +506,13 @@
  11.109       val th0 = fconv_rule (Thm.beta_conversion true)
  11.110           (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE)
  11.111       val pv = (Thm.rhs_of o Thm.beta_conversion true) 
  11.112 -           (Thm.capply @{cterm Trueprop} (Thm.capply p v))
  11.113 +           (Thm.apply @{cterm Trueprop} (Thm.apply p v))
  11.114       val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
  11.115      in Thm.implies_elim (Thm.implies_elim th0 th) th1  end
  11.116   | _ => raise THM ("choose",0,[th, th'])
  11.117  
  11.118    fun simple_choose v th = 
  11.119 -     choose v (Thm.assume ((Thm.capply @{cterm Trueprop} o mk_ex v) ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
  11.120 +     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
  11.121  
  11.122   val strip_forall =
  11.123    let fun h (acc, t) =
  11.124 @@ -534,7 +534,7 @@
  11.125    fun absremover ct = (literals_conv [@{term HOL.conj}, @{term HOL.disj}] [] 
  11.126                    (try_conv (absconv1 then_conv binop_conv (arg_conv poly_conv))) then_conv 
  11.127          try_conv (absconv2 then_conv nnf_norm_conv' then_conv binop_conv absremover)) ct
  11.128 -  val nct = Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"} ct)
  11.129 +  val nct = Thm.apply @{cterm Trueprop} (Thm.apply @{cterm "Not"} ct)
  11.130    val th0 = (init_conv then_conv arg_conv nnf_norm_conv') nct
  11.131    val tm0 = Thm.dest_arg (Thm.rhs_of th0)
  11.132    val (th, certificates) = if tm0 aconvc @{cterm False} then (equal_implies_1_rule th0, Trivial) else
  11.133 @@ -543,7 +543,7 @@
  11.134      val (avs,ibod) = strip_forall bod
  11.135      val th1 = Drule.arg_cong_rule @{cterm Trueprop} (fold mk_forall avs (absremover ibod))
  11.136      val (th2, certs) = overall [] [] [specl avs (Thm.assume (Thm.rhs_of th1))]
  11.137 -    val th3 = fold simple_choose evs (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.capply @{cterm Trueprop} bod))) th2)
  11.138 +    val th3 = fold simple_choose evs (prove_hyp (Thm.equal_elim th1 (Thm.assume (Thm.apply @{cterm Trueprop} bod))) th2)
  11.139     in (Drule.implies_intr_hyps (prove_hyp (Thm.equal_elim th0 (Thm.assume nct)) th3), certs)
  11.140     end
  11.141    in (Thm.implies_elim (instantiate' [] [SOME ct] pth_final) th, certificates)
  11.142 @@ -699,7 +699,7 @@
  11.143     fun eliminate_construct p c tm =
  11.144      let 
  11.145       val t = find_cterm p tm
  11.146 -     val th0 = (Thm.symmetric o Thm.beta_conversion false) (Thm.capply (Thm.cabs t tm) t)
  11.147 +     val th0 = (Thm.symmetric o Thm.beta_conversion false) (Thm.apply (Thm.lambda t tm) t)
  11.148       val (p,ax) = (Thm.dest_comb o Thm.rhs_of) th0
  11.149      in fconv_rule(arg_conv(binop_conv (arg_conv (Thm.beta_conversion false))))
  11.150                 (Thm.transitive th0 (c p ax))
    12.1 --- a/src/HOL/Multivariate_Analysis/normarith.ML	Wed Feb 15 22:44:31 2012 +0100
    12.2 +++ b/src/HOL/Multivariate_Analysis/normarith.ML	Wed Feb 15 23:19:30 2012 +0100
    12.3 @@ -149,7 +149,7 @@
    12.4  let val (a, b) = Rat.quotient_of_rat x
    12.5  in
    12.6   if b = 1 then Numeral.mk_cnumber @{ctyp "real"} a
    12.7 -  else Thm.capply (Thm.capply @{cterm "op / :: real => _"}
    12.8 +  else Thm.apply (Thm.apply @{cterm "op / :: real => _"}
    12.9                     (Numeral.mk_cnumber @{ctyp "real"} a))
   12.10          (Numeral.mk_cnumber @{ctyp "real"} b)
   12.11  end;
   12.12 @@ -335,8 +335,8 @@
   12.13    val lctab = vector_lincombs (map snd (filter (not o fst) ntms))
   12.14    val (fxns, ctxt') = Variable.variant_fixes (replicate (length lctab) "x") ctxt
   12.15    fun instantiate_cterm' ty tms = Drule.cterm_rule (Drule.instantiate' ty tms)
   12.16 -  fun mk_norm t = Thm.capply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
   12.17 -  fun mk_equals l r = Thm.capply (Thm.capply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r
   12.18 +  fun mk_norm t = Thm.apply (instantiate_cterm' [SOME (ctyp_of_term t)] [] @{cpat "norm :: (?'a :: real_normed_vector) => real"}) t
   12.19 +  fun mk_equals l r = Thm.apply (Thm.apply (instantiate_cterm' [SOME (ctyp_of_term l)] [] @{cpat "op == :: ?'a =>_"}) l) r
   12.20    val asl = map2 (fn (t,_) => fn n => Thm.assume (mk_equals (mk_norm t) (cterm_of (Proof_Context.theory_of ctxt') (Free(n,@{typ real}))))) lctab fxns
   12.21    val replace_conv = try_conv (rewrs_conv asl)
   12.22    val replace_rule = fconv_rule (funpow 2 arg_conv (replacenegnorms replace_conv))
    13.1 --- a/src/HOL/Tools/Meson/meson_clausify.ML	Wed Feb 15 22:44:31 2012 +0100
    13.2 +++ b/src/HOL/Tools/Meson/meson_clausify.ML	Wed Feb 15 23:19:30 2012 +0100
    13.3 @@ -155,7 +155,7 @@
    13.4        val (v, _) = dest_Free (term_of cv)
    13.5        val u_th = introduce_combinators_in_cterm cta
    13.6        val cu = Thm.rhs_of u_th
    13.7 -      val comb_eq = abstract (Thm.cabs cv cu)
    13.8 +      val comb_eq = abstract (Thm.lambda cv cu)
    13.9      in Thm.transitive (Thm.abstract_rule v cv u_th) comb_eq end
   13.10    | _ $ _ =>
   13.11      let val (ct1, ct2) = Thm.dest_comb ct in
   13.12 @@ -205,10 +205,10 @@
   13.13        | _ => raise TERM ("old_skolem_theorem_from_def: expected \"Eps\"",
   13.14                           [hilbert])
   13.15      val cex = cterm_of thy (HOLogic.exists_const T)
   13.16 -    val ex_tm = Thm.capply cTrueprop (Thm.capply cex cabs)
   13.17 +    val ex_tm = Thm.apply cTrueprop (Thm.apply cex cabs)
   13.18      val conc =
   13.19        Drule.list_comb (rhs, frees)
   13.20 -      |> Drule.beta_conv cabs |> Thm.capply cTrueprop
   13.21 +      |> Drule.beta_conv cabs |> Thm.apply cTrueprop
   13.22      fun tacf [prem] =
   13.23        rewrite_goals_tac skolem_def_raw
   13.24        THEN rtac ((prem |> rewrite_rule skolem_def_raw)
    14.1 --- a/src/HOL/Tools/Qelim/cooper.ML	Wed Feb 15 22:44:31 2012 +0100
    14.2 +++ b/src/HOL/Tools/Qelim/cooper.ML	Wed Feb 15 23:19:30 2012 +0100
    14.3 @@ -144,7 +144,7 @@
    14.4    let val (x,eq) =
    14.5       (Thm.dest_abs NONE o Thm.dest_arg o snd o Thm.dest_abs NONE o Thm.dest_arg)
    14.6          (Thm.dest_arg t)
    14.7 -in (Thm.cabs x o Thm.dest_arg o Thm.dest_arg) eq end;
    14.8 +in (Thm.lambda x o Thm.dest_arg o Thm.dest_arg) eq end;
    14.9  
   14.10  val get_pmi = get_pmi_term o cprop_of;
   14.11  
   14.12 @@ -179,15 +179,15 @@
   14.13  fun numeral2 f m n = HOLogic.mk_number iT (f (dest_number m) (dest_number n));
   14.14  
   14.15  val [minus1,plus1] =
   14.16 -    map (fn c => fn t => Thm.capply (Thm.capply c t) cone) [cminus,cadd];
   14.17 +    map (fn c => fn t => Thm.apply (Thm.apply c t) cone) [cminus,cadd];
   14.18  
   14.19  fun decomp_pinf x dvd inS [aseteq, asetneq, asetlt, asetle,
   14.20                             asetgt, asetge,asetdvd,asetndvd,asetP,
   14.21                             infDdvd, infDndvd, asetconj,
   14.22                             asetdisj, infDconj, infDdisj] cp =
   14.23   case (whatis x cp) of
   14.24 -  And (p,q) => ([p,q], myfwd (piconj, asetconj, infDconj) (Thm.cabs x p) (Thm.cabs x q))
   14.25 -| Or (p,q) => ([p,q], myfwd (pidisj, asetdisj, infDdisj) (Thm.cabs x p) (Thm.cabs x q))
   14.26 +  And (p,q) => ([p,q], myfwd (piconj, asetconj, infDconj) (Thm.lambda x p) (Thm.lambda x q))
   14.27 +| Or (p,q) => ([p,q], myfwd (pidisj, asetdisj, infDdisj) (Thm.lambda x p) (Thm.lambda x q))
   14.28  | Eq t => ([], K (inst' [t] pieq, FWD (inst' [t] aseteq) [inS (plus1 t)], infDFalse))
   14.29  | NEq t => ([], K (inst' [t] pineq, FWD (inst' [t] asetneq) [inS t], infDTrue))
   14.30  | Lt t => ([], K (inst' [t] pilt, FWD (inst' [t] asetlt) [inS t], infDFalse))
   14.31 @@ -206,8 +206,8 @@
   14.32                             infDdvd, infDndvd, bsetconj,
   14.33                             bsetdisj, infDconj, infDdisj] cp =
   14.34   case (whatis x cp) of
   14.35 -  And (p,q) => ([p,q], myfwd (miconj, bsetconj, infDconj) (Thm.cabs x p) (Thm.cabs x q))
   14.36 -| Or (p,q) => ([p,q], myfwd (midisj, bsetdisj, infDdisj) (Thm.cabs x p) (Thm.cabs x q))
   14.37 +  And (p,q) => ([p,q], myfwd (miconj, bsetconj, infDconj) (Thm.lambda x p) (Thm.lambda x q))
   14.38 +| Or (p,q) => ([p,q], myfwd (midisj, bsetdisj, infDdisj) (Thm.lambda x p) (Thm.lambda x q))
   14.39  | Eq t => ([], K (inst' [t] mieq, FWD (inst' [t] bseteq) [inS (minus1 t)], infDFalse))
   14.40  | NEq t => ([], K (inst' [t] mineq, FWD (inst' [t] bsetneq) [inS t], infDTrue))
   14.41  | Lt t => ([], K (inst' [t] milt, (inst' [t] bsetlt), infDTrue))
   14.42 @@ -368,8 +368,8 @@
   14.43     let
   14.44      val th =
   14.45       Simplifier.rewrite lin_ss
   14.46 -      (Thm.capply @{cterm Trueprop} (Thm.capply @{cterm "Not"}
   14.47 -           (Thm.capply (Thm.capply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x))
   14.48 +      (Thm.apply @{cterm Trueprop} (Thm.apply @{cterm "Not"}
   14.49 +           (Thm.apply (Thm.apply @{cterm "op = :: int => _"} (Numeral.mk_cnumber @{ctyp "int"} x))
   14.50             @{cterm "0::int"})))
   14.51     in Thm.equal_elim (Thm.symmetric th) TrueI end;
   14.52    val notz =
   14.53 @@ -411,9 +411,9 @@
   14.54    | _ => Thm.reflexive t
   14.55    val uth = unit_conv p
   14.56    val clt =  Numeral.mk_cnumber @{ctyp "int"} l
   14.57 -  val ltx = Thm.capply (Thm.capply cmulC clt) cx
   14.58 +  val ltx = Thm.apply (Thm.apply cmulC clt) cx
   14.59    val th = Drule.arg_cong_rule e (Thm.abstract_rule (fst (dest_Free x )) cx uth)
   14.60 -  val th' = inst' [Thm.cabs ltx (Thm.rhs_of uth), clt] unity_coeff_ex
   14.61 +  val th' = inst' [Thm.lambda ltx (Thm.rhs_of uth), clt] unity_coeff_ex
   14.62    val thf = Thm.transitive th
   14.63        (Thm.transitive (Thm.symmetric (Thm.beta_conversion true (cprop_of th' |> Thm.dest_arg1))) th')
   14.64    val (lth,rth) = Thm.dest_comb (cprop_of thf) |>> Thm.dest_arg |>> Thm.beta_conversion true
   14.65 @@ -423,7 +423,7 @@
   14.66  
   14.67  val emptyIS = @{cterm "{}::int set"};
   14.68  val insert_tm = @{cterm "insert :: int => _"};
   14.69 -fun mkISet cts = fold_rev (Thm.capply insert_tm #> Thm.capply) cts emptyIS;
   14.70 +fun mkISet cts = fold_rev (Thm.apply insert_tm #> Thm.apply) cts emptyIS;
   14.71  val eqelem_imp_imp = @{thm eqelem_imp_iff} RS iffD1;
   14.72  val [A_tm,B_tm] = map (fn th => cprop_of th |> funpow 2 Thm.dest_arg |> Thm.dest_abs NONE |> snd |> Thm.dest_arg1 |> Thm.dest_arg
   14.73                                        |> Thm.dest_abs NONE |> snd |> Thm.dest_fun |> Thm.dest_arg)
   14.74 @@ -459,8 +459,8 @@
   14.75     let
   14.76      val th =
   14.77       Simplifier.rewrite lin_ss
   14.78 -      (Thm.capply @{cterm Trueprop}
   14.79 -           (Thm.capply (Thm.capply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd))
   14.80 +      (Thm.apply @{cterm Trueprop}
   14.81 +           (Thm.apply (Thm.apply dvdc (Numeral.mk_cnumber @{ctyp "int"} x)) cd))
   14.82     in Thm.equal_elim (Thm.symmetric th) TrueI end;
   14.83   val dvd =
   14.84     let val tab = fold Inttab.update (ds ~~ (map divprop ds)) Inttab.empty in
   14.85 @@ -471,8 +471,8 @@
   14.86     end
   14.87   val dp =
   14.88     let val th = Simplifier.rewrite lin_ss
   14.89 -      (Thm.capply @{cterm Trueprop}
   14.90 -           (Thm.capply (Thm.capply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd))
   14.91 +      (Thm.apply @{cterm Trueprop}
   14.92 +           (Thm.apply (Thm.apply @{cterm "op < :: int => _"} @{cterm "0::int"}) cd))
   14.93     in Thm.equal_elim (Thm.symmetric th) TrueI end;
   14.94      (* A and B set *)
   14.95     local
   14.96 @@ -714,9 +714,9 @@
   14.97       val (ps, c) = split_last (strip_objimp p)
   14.98       val qs = filter P ps
   14.99       val q = if P c then c else @{cterm "False"}
  14.100 -     val ng = fold_rev (fn (a,v) => fn t => Thm.capply a (Thm.cabs v t)) qvs 
  14.101 -         (fold_rev (fn p => fn q => Thm.capply (Thm.capply @{cterm HOL.implies} p) q) qs q)
  14.102 -     val g = Thm.capply (Thm.capply @{cterm "op ==>"} (Thm.capply @{cterm "Trueprop"} ng)) p'
  14.103 +     val ng = fold_rev (fn (a,v) => fn t => Thm.apply a (Thm.lambda v t)) qvs 
  14.104 +         (fold_rev (fn p => fn q => Thm.apply (Thm.apply @{cterm HOL.implies} p) q) qs q)
  14.105 +     val g = Thm.apply (Thm.apply @{cterm "op ==>"} (Thm.apply @{cterm "Trueprop"} ng)) p'
  14.106       val ntac = (case qs of [] => q aconvc @{cterm "False"}
  14.107                           | _ => false)
  14.108      in 
  14.109 @@ -777,7 +777,7 @@
  14.110  fun generalize_tac f = CSUBGOAL (fn (p, i) => PRIMITIVE (fn st =>
  14.111   let 
  14.112     fun all T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "all"}
  14.113 -   fun gen x t = Thm.capply (all (ctyp_of_term x)) (Thm.cabs x t)
  14.114 +   fun gen x t = Thm.apply (all (ctyp_of_term x)) (Thm.lambda x t)
  14.115     val ts = sort (fn (a,b) => Term_Ord.fast_term_ord (term_of a, term_of b)) (f p)
  14.116     val p' = fold_rev gen ts p
  14.117   in Thm.implies_intr p' (Thm.implies_elim st (fold Thm.forall_elim ts (Thm.assume p'))) end));
    15.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Wed Feb 15 22:44:31 2012 +0100
    15.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Wed Feb 15 23:19:30 2012 +0100
    15.3 @@ -196,7 +196,7 @@
    15.4  
    15.5    val pat =
    15.6      SMT_Utils.mk_const_pat @{theory} @{const_name SMT.pat} SMT_Utils.destT1
    15.7 -  fun mk_pat ct = Thm.capply (SMT_Utils.instT' ct pat) ct
    15.8 +  fun mk_pat ct = Thm.apply (SMT_Utils.instT' ct pat) ct
    15.9  
   15.10    fun mk_clist T = pairself (Thm.cterm_of @{theory})
   15.11      (HOLogic.cons_const T, HOLogic.nil_const T)
    16.1 --- a/src/HOL/Tools/SMT/smt_real.ML	Wed Feb 15 22:44:31 2012 +0100
    16.2 +++ b/src/HOL/Tools/SMT/smt_real.ML	Wed Feb 15 23:19:30 2012 +0100
    16.3 @@ -67,7 +67,7 @@
    16.4      if T = @{typ real} then SOME (Numeral.mk_cnumber @{ctyp real} i)
    16.5      else NONE
    16.6  
    16.7 -  val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (real)})
    16.8 +  val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (real)})
    16.9    val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (real)})
   16.10    val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (real)})
   16.11    val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (real)})
    17.1 --- a/src/HOL/Tools/SMT/smt_solver.ML	Wed Feb 15 22:44:31 2012 +0100
    17.2 +++ b/src/HOL/Tools/SMT/smt_solver.ML	Wed Feb 15 23:19:30 2012 +0100
    17.3 @@ -283,7 +283,7 @@
    17.4  
    17.5      val {facts, goal, ...} = Proof.goal st
    17.6      val ({context=ctxt', prems, concl, ...}, _) = Subgoal.focus ctxt i goal
    17.7 -    fun negate ct = Thm.dest_comb ct ||> Thm.capply cnot |-> Thm.capply
    17.8 +    fun negate ct = Thm.dest_comb ct ||> Thm.apply cnot |-> Thm.apply
    17.9      val cprop =
   17.10        (case try negate (Thm.rhs_of (SMT_Normalize.atomize_conv ctxt' concl)) of
   17.11          SOME ct => ct
    18.1 --- a/src/HOL/Tools/SMT/smt_utils.ML	Wed Feb 15 22:44:31 2012 +0100
    18.2 +++ b/src/HOL/Tools/SMT/smt_utils.ML	Wed Feb 15 23:19:30 2012 +0100
    18.3 @@ -182,7 +182,7 @@
    18.4  
    18.5  val dest_all_cbinders = repeat_yield (try o dest_cbinder)
    18.6  
    18.7 -val mk_cprop = Thm.capply (Thm.cterm_of @{theory} @{const Trueprop})
    18.8 +val mk_cprop = Thm.apply (Thm.cterm_of @{theory} @{const Trueprop})
    18.9  
   18.10  fun dest_cprop ct =
   18.11    (case Thm.term_of ct of
    19.1 --- a/src/HOL/Tools/SMT/z3_interface.ML	Wed Feb 15 22:44:31 2012 +0100
    19.2 +++ b/src/HOL/Tools/SMT/z3_interface.ML	Wed Feb 15 23:19:30 2012 +0100
    19.3 @@ -138,7 +138,7 @@
    19.4  
    19.5  val mk_true = Thm.cterm_of @{theory} (@{const Not} $ @{const False})
    19.6  val mk_false = Thm.cterm_of @{theory} @{const False}
    19.7 -val mk_not = Thm.capply (Thm.cterm_of @{theory} @{const Not})
    19.8 +val mk_not = Thm.apply (Thm.cterm_of @{theory} @{const Not})
    19.9  val mk_implies = Thm.mk_binop (Thm.cterm_of @{theory} @{const HOL.implies})
   19.10  val mk_iff = Thm.mk_binop (Thm.cterm_of @{theory} @{const HOL.eq (bool)})
   19.11  val conj = Thm.cterm_of @{theory} @{const HOL.conj}
   19.12 @@ -154,7 +154,7 @@
   19.13    SMT_Utils.mk_const_pat @{theory} @{const_name If}
   19.14      (SMT_Utils.destT1 o SMT_Utils.destT2)
   19.15  fun mk_if cc ct cu =
   19.16 -  Thm.mk_binop (Thm.capply (SMT_Utils.instT' ct if_term) cc) ct cu
   19.17 +  Thm.mk_binop (Thm.apply (SMT_Utils.instT' ct if_term) cc) ct cu
   19.18  
   19.19  val nil_term =
   19.20    SMT_Utils.mk_const_pat @{theory} @{const_name Nil} SMT_Utils.destT1
   19.21 @@ -168,22 +168,22 @@
   19.22    (SMT_Utils.destT1 o SMT_Utils.destT1)
   19.23  fun mk_distinct [] = mk_true
   19.24    | mk_distinct (cts as (ct :: _)) =
   19.25 -      Thm.capply (SMT_Utils.instT' ct distinct)
   19.26 +      Thm.apply (SMT_Utils.instT' ct distinct)
   19.27          (mk_list (Thm.ctyp_of_term ct) cts)
   19.28  
   19.29  val access =
   19.30    SMT_Utils.mk_const_pat @{theory} @{const_name fun_app} SMT_Utils.destT1
   19.31 -fun mk_access array = Thm.capply (SMT_Utils.instT' array access) array
   19.32 +fun mk_access array = Thm.apply (SMT_Utils.instT' array access) array
   19.33  
   19.34  val update = SMT_Utils.mk_const_pat @{theory} @{const_name fun_upd}
   19.35    (Thm.dest_ctyp o SMT_Utils.destT1)
   19.36  fun mk_update array index value =
   19.37    let val cTs = Thm.dest_ctyp (Thm.ctyp_of_term array)
   19.38    in
   19.39 -    Thm.capply (Thm.mk_binop (SMT_Utils.instTs cTs update) array index) value
   19.40 +    Thm.apply (Thm.mk_binop (SMT_Utils.instTs cTs update) array index) value
   19.41    end
   19.42  
   19.43 -val mk_uminus = Thm.capply (Thm.cterm_of @{theory} @{const uminus (int)})
   19.44 +val mk_uminus = Thm.apply (Thm.cterm_of @{theory} @{const uminus (int)})
   19.45  val mk_add = Thm.mk_binop (Thm.cterm_of @{theory} @{const plus (int)})
   19.46  val mk_sub = Thm.mk_binop (Thm.cterm_of @{theory} @{const minus (int)})
   19.47  val mk_mul = Thm.mk_binop (Thm.cterm_of @{theory} @{const times (int)})
   19.48 @@ -207,7 +207,7 @@
   19.49    | (Sym ("ite", _), [ct1, ct2, ct3]) => SOME (mk_if ct1 ct2 ct3) (* FIXME: remove *)
   19.50    | (Sym ("=", _), [ct, cu]) => SOME (mk_eq ct cu)
   19.51    | (Sym ("distinct", _), _) => SOME (mk_distinct cts)
   19.52 -  | (Sym ("select", _), [ca, ck]) => SOME (Thm.capply (mk_access ca) ck)
   19.53 +  | (Sym ("select", _), [ca, ck]) => SOME (Thm.apply (mk_access ca) ck)
   19.54    | (Sym ("store", _), [ca, ck, cv]) => SOME (mk_update ca ck cv)
   19.55    | _ =>
   19.56      (case (sym, try (#T o Thm.rep_cterm o hd) cts, cts) of
    20.1 --- a/src/HOL/Tools/SMT/z3_proof_literals.ML	Wed Feb 15 22:44:31 2012 +0100
    20.2 +++ b/src/HOL/Tools/SMT/z3_proof_literals.ML	Wed Feb 15 23:19:30 2012 +0100
    20.3 @@ -82,7 +82,7 @@
    20.4        | NONE => false)
    20.5    in exists end
    20.6  
    20.7 -val negate = Thm.capply (Thm.cterm_of @{theory} @{const Not})
    20.8 +val negate = Thm.apply (Thm.cterm_of @{theory} @{const Not})
    20.9  
   20.10  
   20.11  
    21.1 --- a/src/HOL/Tools/SMT/z3_proof_methods.ML	Wed Feb 15 22:44:31 2012 +0100
    21.2 +++ b/src/HOL/Tools/SMT/z3_proof_methods.ML	Wed Feb 15 23:19:30 2012 +0100
    21.3 @@ -109,7 +109,7 @@
    21.4        SMT_Utils.dest_all_cbinders (SMT_Utils.dest_cprop rhs) ctxt
    21.5      val (cl, cv) = Thm.dest_binop ct
    21.6      val (cg, (cargs, cf)) = Drule.strip_comb cl ||> split_last
    21.7 -    val cu = fold_rev Thm.cabs cargs (mk_inv_of ctxt' (Thm.cabs cv cf))
    21.8 +    val cu = fold_rev Thm.lambda cargs (mk_inv_of ctxt' (Thm.lambda cv cf))
    21.9    in Thm.assume (SMT_Utils.mk_cequals cg cu) end
   21.10  
   21.11  fun prove_inj_eq ctxt ct =
    22.1 --- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Wed Feb 15 22:44:31 2012 +0100
    22.2 +++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Wed Feb 15 23:19:30 2012 +0100
    22.3 @@ -134,7 +134,7 @@
    22.4          | _ => SMT_Utils.certify ctxt (Var ((Name.uu, maxidx_of ct + 1), T)))
    22.5        fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v)
    22.6        val vars' = map_filter dec vars
    22.7 -    in (Thm.capply (SMT_Utils.instT' cv q) (Thm.cabs cv ct), vars') end
    22.8 +    in (Thm.apply (SMT_Utils.instT' cv q) (Thm.lambda cv ct), vars') end
    22.9  
   22.10    fun quant name =
   22.11      SMT_Utils.mk_const_pat @{theory} name (SMT_Utils.destT1 o SMT_Utils.destT1)
    23.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Wed Feb 15 22:44:31 2012 +0100
    23.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Wed Feb 15 23:19:30 2012 +0100
    23.3 @@ -618,7 +618,7 @@
    23.4      SMT_Utils.mk_const_pat @{theory} @{const_name all}
    23.5        (SMT_Utils.destT1 o SMT_Utils.destT1)
    23.6    fun mk_forall cv ct =
    23.7 -    Thm.capply (SMT_Utils.instT' cv forall) (Thm.cabs cv ct)
    23.8 +    Thm.apply (SMT_Utils.instT' cv forall) (Thm.lambda cv ct)
    23.9  
   23.10    fun get_vars f mk pred ctxt t =
   23.11      Term.fold_aterms f t []
    24.1 --- a/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Feb 15 22:44:31 2012 +0100
    24.2 +++ b/src/HOL/Tools/SMT/z3_proof_tools.ML	Wed Feb 15 23:19:30 2012 +0100
    24.3 @@ -116,7 +116,7 @@
    24.4    let
    24.5      val (lhs, rhs) = Thm.dest_binop (Thm.cprem_of thm 1)
    24.6      val (cf, cvs) = Drule.strip_comb lhs
    24.7 -    val eq = SMT_Utils.mk_cequals cf (fold_rev Thm.cabs cvs rhs)
    24.8 +    val eq = SMT_Utils.mk_cequals cf (fold_rev Thm.lambda cvs rhs)
    24.9      fun apply cv th =
   24.10        Thm.combination th (Thm.reflexive cv)
   24.11        |> Conv.fconv_rule (Conv.arg_conv (Thm.beta_conversion false))
   24.12 @@ -159,14 +159,14 @@
   24.13            val cv = SMT_Utils.certify ctxt'
   24.14              (Free (n, map SMT_Utils.typ_of cvs' ---> SMT_Utils.typ_of ct))
   24.15            val cu = Drule.list_comb (cv, cvs')
   24.16 -          val e = (t, (cv, fold_rev Thm.cabs cvs' ct))
   24.17 +          val e = (t, (cv, fold_rev Thm.lambda cvs' ct))
   24.18            val beta_norm' = beta_norm orelse not (null cvs')
   24.19          in (cu, (ctxt', Termtab.update e tab, idx + 1, beta_norm')) end)
   24.20    end
   24.21  
   24.22  fun abs_comb f g dcvs ct =
   24.23    let val (cf, cu) = Thm.dest_comb ct
   24.24 -  in f dcvs cf ##>> g dcvs cu #>> uncurry Thm.capply end
   24.25 +  in f dcvs cf ##>> g dcvs cu #>> uncurry Thm.apply end
   24.26  
   24.27  fun abs_arg f = abs_comb (K pair) f
   24.28  
   24.29 @@ -184,7 +184,7 @@
   24.30  
   24.31  fun abs_abs f (depth, cvs) ct =
   24.32    let val (cv, cu) = Thm.dest_abs NONE ct
   24.33 -  in f (depth, cv :: cvs) cu #>> Thm.cabs cv end
   24.34 +  in f (depth, cv :: cvs) cu #>> Thm.lambda cv end
   24.35  
   24.36  val is_atomic =
   24.37    (fn Free _ => true | Var _ => true | Bound _ => true | _ => false)
    25.1 --- a/src/HOL/Tools/TFL/dcterm.ML	Wed Feb 15 22:44:31 2012 +0100
    25.2 +++ b/src/HOL/Tools/TFL/dcterm.ML	Wed Feb 15 23:19:30 2012 +0100
    25.3 @@ -56,10 +56,10 @@
    25.4  fun dest_abs a t = Thm.dest_abs a t
    25.5    handle CTERM (msg, _) => raise ERR "dest_abs" msg;
    25.6  
    25.7 -fun capply t u = Thm.capply t u
    25.8 +fun capply t u = Thm.apply t u
    25.9    handle CTERM (msg, _) => raise ERR "capply" msg;
   25.10  
   25.11 -fun cabs a t = Thm.cabs a t
   25.12 +fun cabs a t = Thm.lambda a t
   25.13    handle CTERM (msg, _) => raise ERR "cabs" msg;
   25.14  
   25.15  
    26.1 --- a/src/HOL/Tools/groebner.ML	Wed Feb 15 22:44:31 2012 +0100
    26.2 +++ b/src/HOL/Tools/groebner.ML	Wed Feb 15 23:19:30 2012 +0100
    26.3 @@ -395,7 +395,7 @@
    26.4    | _ => rfn tm ;
    26.5  
    26.6  val notnotD = @{thm notnotD};
    26.7 -fun mk_binop ct x y = Thm.capply (Thm.capply ct x) y
    26.8 +fun mk_binop ct x y = Thm.apply (Thm.apply ct x) y
    26.9  
   26.10  fun is_neg t =
   26.11      case term_of t of
   26.12 @@ -451,10 +451,10 @@
   26.13  val cTrp = @{cterm "Trueprop"};
   26.14  val cConj = @{cterm HOL.conj};
   26.15  val (cNot,false_tm) = (@{cterm "Not"}, @{cterm "False"});
   26.16 -val assume_Trueprop = Thm.capply cTrp #> Thm.assume;
   26.17 +val assume_Trueprop = Thm.apply cTrp #> Thm.assume;
   26.18  val list_mk_conj = list_mk_binop cConj;
   26.19  val conjs = list_dest_binop cConj;
   26.20 -val mk_neg = Thm.capply cNot;
   26.21 +val mk_neg = Thm.apply cNot;
   26.22  
   26.23  fun striplist dest =
   26.24   let
   26.25 @@ -462,7 +462,7 @@
   26.26      SOME (a,b) => h (h acc b) a
   26.27    | NONE => x::acc
   26.28   in h [] end;
   26.29 -fun list_mk_binop b = foldr1 (fn (s,t) => Thm.capply (Thm.capply b s) t);
   26.30 +fun list_mk_binop b = foldr1 (fn (s,t) => Thm.apply (Thm.apply b s) t);
   26.31  
   26.32  val eq_commute = mk_meta_eq @{thm eq_commute};
   26.33  
   26.34 @@ -479,7 +479,7 @@
   26.35  
   26.36  fun fold1 f = foldr1 (uncurry f);
   26.37  
   26.38 -val list_conj = fold1 (fn c => fn c' => Thm.capply (Thm.capply @{cterm HOL.conj} c) c') ;
   26.39 +val list_conj = fold1 (fn c => fn c' => Thm.apply (Thm.apply @{cterm HOL.conj} c) c') ;
   26.40  
   26.41  fun mk_conj_tab th =
   26.42   let fun h acc th =
   26.43 @@ -500,8 +500,8 @@
   26.44  fun conj_ac_rule eq =
   26.45   let
   26.46    val (l,r) = Thm.dest_equals eq
   26.47 -  val ctabl = mk_conj_tab (Thm.assume (Thm.capply @{cterm Trueprop} l))
   26.48 -  val ctabr = mk_conj_tab (Thm.assume (Thm.capply @{cterm Trueprop} r))
   26.49 +  val ctabl = mk_conj_tab (Thm.assume (Thm.apply @{cterm Trueprop} l))
   26.50 +  val ctabr = mk_conj_tab (Thm.assume (Thm.apply @{cterm Trueprop} r))
   26.51    fun tabl c = the (Termtab.lookup ctabl (term_of c))
   26.52    fun tabr c = the (Termtab.lookup ctabr (term_of c))
   26.53    val thl  = prove_conj tabl (conjuncts r) |> implies_intr_hyps
   26.54 @@ -514,7 +514,7 @@
   26.55     (* Conversion for the equivalence of existential statements where
   26.56        EX quantifiers are rearranged differently *)
   26.57   fun ext T = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat Ex}
   26.58 - fun mk_ex v t = Thm.capply (ext (ctyp_of_term v)) (Thm.cabs v t)
   26.59 + fun mk_ex v t = Thm.apply (ext (ctyp_of_term v)) (Thm.lambda v t)
   26.60  
   26.61  fun choose v th th' = case concl_of th of
   26.62    @{term Trueprop} $ (Const(@{const_name Ex},_)$_) =>
   26.63 @@ -524,19 +524,19 @@
   26.64      val th0 = Conv.fconv_rule (Thm.beta_conversion true)
   26.65          (instantiate' [SOME T] [SOME p, (SOME o Thm.dest_arg o cprop_of) th'] exE)
   26.66      val pv = (Thm.rhs_of o Thm.beta_conversion true)
   26.67 -          (Thm.capply @{cterm Trueprop} (Thm.capply p v))
   26.68 +          (Thm.apply @{cterm Trueprop} (Thm.apply p v))
   26.69      val th1 = Thm.forall_intr v (Thm.implies_intr pv th')
   26.70     in Thm.implies_elim (Thm.implies_elim th0 th) th1  end
   26.71  | _ => error ""  (* FIXME ? *)
   26.72  
   26.73  fun simple_choose v th =
   26.74 -   choose v (Thm.assume ((Thm.capply @{cterm Trueprop} o mk_ex v)
   26.75 +   choose v (Thm.assume ((Thm.apply @{cterm Trueprop} o mk_ex v)
   26.76      ((Thm.dest_arg o hd o #hyps o Thm.crep_thm) th))) th
   26.77  
   26.78  
   26.79   fun mkexi v th =
   26.80    let
   26.81 -   val p = Thm.cabs v (Thm.dest_arg (Thm.cprop_of th))
   26.82 +   val p = Thm.lambda v (Thm.dest_arg (Thm.cprop_of th))
   26.83    in Thm.implies_elim
   26.84      (Conv.fconv_rule (Thm.beta_conversion true)
   26.85        (instantiate' [SOME (ctyp_of_term v)] [SOME p, SOME v] @{thm exI}))
   26.86 @@ -547,7 +547,7 @@
   26.87    val (p0,q0) = Thm.dest_binop t
   26.88    val (vs',P) = strip_exists p0
   26.89    val (vs,_) = strip_exists q0
   26.90 -   val th = Thm.assume (Thm.capply @{cterm Trueprop} P)
   26.91 +   val th = Thm.assume (Thm.apply @{cterm Trueprop} P)
   26.92     val th1 = implies_intr_hyps (fold simple_choose vs' (fold mkexi vs th))
   26.93     val th2 = implies_intr_hyps (fold simple_choose vs (fold mkexi vs' th))
   26.94     val p = (Thm.dest_arg o Thm.dest_arg1 o cprop_of) th1
   26.95 @@ -561,8 +561,8 @@
   26.96    Free(s,_) => s
   26.97   | Var ((s,_),_) => s
   26.98   | _ => "x"
   26.99 - fun mk_eq s t = Thm.capply (Thm.capply @{cterm "op == :: bool => _"} s) t
  26.100 - fun mkeq s t = Thm.capply @{cterm Trueprop} (Thm.capply (Thm.capply @{cterm "op = :: bool => _"} s) t)
  26.101 + fun mk_eq s t = Thm.apply (Thm.apply @{cterm "op == :: bool => _"} s) t
  26.102 + fun mkeq s t = Thm.apply @{cterm Trueprop} (Thm.apply (Thm.apply @{cterm "op = :: bool => _"} s) t)
  26.103   fun mk_exists v th = Drule.arg_cong_rule (ext (ctyp_of_term v))
  26.104     (Thm.abstract_rule (getname v) v th)
  26.105   val simp_ex_conv =
  26.106 @@ -573,7 +573,7 @@
  26.107  
  26.108  val vsubst = let
  26.109   fun vsubst (t,v) tm =
  26.110 -   (Thm.rhs_of o Thm.beta_conversion false) (Thm.capply (Thm.cabs v tm) t)
  26.111 +   (Thm.rhs_of o Thm.beta_conversion false) (Thm.apply (Thm.lambda v tm) t)
  26.112  in fold vsubst end;
  26.113  
  26.114  
  26.115 @@ -607,7 +607,7 @@
  26.116         else raise CTERM ("ring_dest_neg", [t])
  26.117      end
  26.118  
  26.119 - val ring_mk_neg = fn tm => Thm.capply (ring_neg_tm) (tm);
  26.120 + val ring_mk_neg = fn tm => Thm.apply (ring_neg_tm) (tm);
  26.121   fun field_dest_inv t =
  26.122      let val (l,r) = Thm.dest_comb t in
  26.123          if Term.could_unify(term_of l, term_of field_inv_tm) then r
  26.124 @@ -727,7 +727,7 @@
  26.125            ((Conv.arg_conv #> Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) th1
  26.126        val conc = th2 |> concl |> Thm.dest_arg
  26.127        val (l,r) = conc |> dest_eq
  26.128 -    in Thm.implies_intr (Thm.capply cTrp tm)
  26.129 +    in Thm.implies_intr (Thm.apply cTrp tm)
  26.130                      (Thm.equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th2))
  26.131                             (Thm.reflexive l |> mk_object_eq))
  26.132      end
  26.133 @@ -758,7 +758,7 @@
  26.134      fun thm_fn pols =
  26.135          if null pols then Thm.reflexive(mk_const rat_0) else
  26.136          end_itlist mk_add
  26.137 -            (map (fn (i,p) => Drule.arg_cong_rule (Thm.capply ring_mul_tm p)
  26.138 +            (map (fn (i,p) => Drule.arg_cong_rule (Thm.apply ring_mul_tm p)
  26.139                (nth eths i |> mk_meta_eq)) pols)
  26.140      val th1 = thm_fn herts_pos
  26.141      val th2 = thm_fn herts_neg
  26.142 @@ -767,7 +767,7 @@
  26.143        Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv o Conv.binop_conv) ring_normalize_conv)
  26.144          (neq_rule l th3)
  26.145      val (l,r) = dest_eq(Thm.dest_arg(concl th4))
  26.146 -   in Thm.implies_intr (Thm.capply cTrp tm)
  26.147 +   in Thm.implies_intr (Thm.apply cTrp tm)
  26.148                          (Thm.equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th4))
  26.149                     (Thm.reflexive l |> mk_object_eq))
  26.150     end
  26.151 @@ -776,9 +776,9 @@
  26.152  fun ring tm =
  26.153   let
  26.154    fun mk_forall x p =
  26.155 -    Thm.capply
  26.156 +    Thm.apply
  26.157        (Drule.cterm_rule (instantiate' [SOME (ctyp_of_term x)] [])
  26.158 -        @{cpat "All:: (?'a => bool) => _"}) (Thm.cabs x p)
  26.159 +        @{cpat "All:: (?'a => bool) => _"}) (Thm.lambda x p)
  26.160    val avs = Thm.add_cterm_frees tm []
  26.161    val P' = fold mk_forall avs tm
  26.162    val th1 = initial_conv(mk_neg P')
  26.163 @@ -892,7 +892,7 @@
  26.164                     (striplist ring_dest_add tm)
  26.165    val cofactors = map (fn v => find_multipliers v vmons) vars
  26.166    val cnc = if null cmons then zero_tm
  26.167 -             else Thm.capply ring_neg_tm
  26.168 +             else Thm.apply ring_neg_tm
  26.169                      (list_mk_binop ring_add_tm cmons)
  26.170    in (cofactors,cnc)
  26.171    end;
    27.1 --- a/src/HOL/Tools/numeral.ML	Wed Feb 15 22:44:31 2012 +0100
    27.2 +++ b/src/HOL/Tools/numeral.ML	Wed Feb 15 23:19:30 2012 +0100
    27.3 @@ -24,7 +24,7 @@
    27.4    | mk_cnumeral ~1 = @{cterm "Int.Min"}
    27.5    | mk_cnumeral i =
    27.6        let val (q, r) = Integer.div_mod i 2 in
    27.7 -        Thm.capply (mk_cbit r) (mk_cnumeral q)
    27.8 +        Thm.apply (mk_cbit r) (mk_cnumeral q)
    27.9        end;
   27.10  
   27.11  
   27.12 @@ -47,7 +47,7 @@
   27.13  
   27.14  fun mk_cnumber T 0 = instT T zeroT zero
   27.15    | mk_cnumber T 1 = instT T oneT one
   27.16 -  | mk_cnumber T i = Thm.capply (instT T numberT number_of) (mk_cnumeral i);
   27.17 +  | mk_cnumber T i = Thm.apply (instT T numberT number_of) (mk_cnumeral i);
   27.18  
   27.19  end;
   27.20  
    28.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Wed Feb 15 22:44:31 2012 +0100
    28.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Wed Feb 15 23:19:30 2012 +0100
    28.3 @@ -566,8 +566,8 @@
    28.4        val z = Thm.instantiate_cterm ([(zT,T)],[]) zr
    28.5        val eq = Thm.instantiate_cterm ([(eqT,T)],[]) geq
    28.6        val th = Simplifier.rewrite (ss addsimps @{thms simp_thms})
    28.7 -           (Thm.capply @{cterm "Trueprop"} (Thm.capply @{cterm "Not"}
    28.8 -                  (Thm.capply (Thm.capply eq t) z)))
    28.9 +           (Thm.apply @{cterm "Trueprop"} (Thm.apply @{cterm "Not"}
   28.10 +                  (Thm.apply (Thm.apply eq t) z)))
   28.11      in Thm.equal_elim (Thm.symmetric th) TrueI
   28.12      end
   28.13  
    29.1 --- a/src/HOL/Tools/semiring_normalizer.ML	Wed Feb 15 22:44:31 2012 +0100
    29.2 +++ b/src/HOL/Tools/semiring_normalizer.ML	Wed Feb 15 23:19:30 2012 +0100
    29.3 @@ -199,8 +199,8 @@
    29.4      fun mk_const phi cT x =
    29.5        let val (a, b) = Rat.quotient_of_rat x
    29.6        in if b = 1 then Numeral.mk_cnumber cT a
    29.7 -        else Thm.capply
    29.8 -             (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
    29.9 +        else Thm.apply
   29.10 +             (Thm.apply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
   29.11                           (Numeral.mk_cnumber cT a))
   29.12               (Numeral.mk_cnumber cT b)
   29.13        end
   29.14 @@ -725,7 +725,7 @@
   29.15  (* Power of polynomial (optimized for the monomial and trivial cases).       *)
   29.16  
   29.17  fun num_conv n =
   29.18 -  nat_add_conv (Thm.capply @{cterm Suc} (Numeral.mk_cnumber @{ctyp nat} (dest_numeral n - 1)))
   29.19 +  nat_add_conv (Thm.apply @{cterm Suc} (Numeral.mk_cnumber @{ctyp nat} (dest_numeral n - 1)))
   29.20    |> Thm.symmetric;
   29.21  
   29.22  
    30.1 --- a/src/HOL/Tools/transfer.ML	Wed Feb 15 22:44:31 2012 +0100
    30.2 +++ b/src/HOL/Tools/transfer.ML	Wed Feb 15 23:19:30 2012 +0100
    30.3 @@ -109,7 +109,7 @@
    30.4      val ([a, D], ctxt2) = ctxt1
    30.5        |> Variable.import true (map Drule.mk_term [raw_a, raw_D])
    30.6        |>> map Drule.dest_term o snd;
    30.7 -    val transform = Thm.capply @{cterm "Trueprop"} o Thm.capply D;
    30.8 +    val transform = Thm.apply @{cterm "Trueprop"} o Thm.apply D;
    30.9      val T = Thm.typ_of (Thm.ctyp_of_term a);
   30.10      val (aT, bT) = (Term.range_type T, Term.domain_type T);
   30.11      
   30.12 @@ -124,7 +124,7 @@
   30.13      val c_vars = map (certify o Var) vars;
   30.14      val (vs', ctxt4) = Variable.variant_fixes (map (fst o fst) vars) ctxt3;
   30.15      val c_vars' = map (certify o (fn v => Free (v, bT))) vs';
   30.16 -    val c_exprs' = map (Thm.capply a) c_vars';
   30.17 +    val c_exprs' = map (Thm.apply a) c_vars';
   30.18  
   30.19      (* transfer *)
   30.20      val (hyps, ctxt5) = ctxt4
    31.1 --- a/src/Pure/conjunction.ML	Wed Feb 15 22:44:31 2012 +0100
    31.2 +++ b/src/Pure/conjunction.ML	Wed Feb 15 23:19:30 2012 +0100
    31.3 @@ -35,7 +35,7 @@
    31.4  val true_prop = certify Logic.true_prop;
    31.5  val conjunction = certify Logic.conjunction;
    31.6  
    31.7 -fun mk_conjunction (A, B) = Thm.capply (Thm.capply conjunction A) B;
    31.8 +fun mk_conjunction (A, B) = Thm.apply (Thm.apply conjunction A) B;
    31.9  
   31.10  fun mk_conjunction_balanced [] = true_prop
   31.11    | mk_conjunction_balanced ts = Balanced_Tree.make mk_conjunction ts;
    32.1 --- a/src/Pure/drule.ML	Wed Feb 15 22:44:31 2012 +0100
    32.2 +++ b/src/Pure/drule.ML	Wed Feb 15 23:19:30 2012 +0100
    32.3 @@ -143,7 +143,7 @@
    32.4  fun certify t = Thm.cterm_of (Context.the_theory (Context.the_thread_data ())) t;
    32.5  
    32.6  val implies = certify Logic.implies;
    32.7 -fun mk_implies (A, B) = Thm.capply (Thm.capply implies A) B;
    32.8 +fun mk_implies (A, B) = Thm.apply (Thm.apply implies A) B;
    32.9  
   32.10  (*cterm version of list_implies: [A1,...,An], B  goes to [|A1;==>;An|]==>B *)
   32.11  fun list_implies([], B) = B
   32.12 @@ -151,7 +151,7 @@
   32.13  
   32.14  (*cterm version of list_comb: maps  (f, [t1,...,tn])  to  f(t1,...,tn) *)
   32.15  fun list_comb (f, []) = f
   32.16 -  | list_comb (f, t::ts) = list_comb (Thm.capply f t, ts);
   32.17 +  | list_comb (f, t::ts) = list_comb (Thm.apply f t, ts);
   32.18  
   32.19  (*cterm version of strip_comb: maps  f(t1,...,tn)  to  (f, [t1,...,tn]) *)
   32.20  fun strip_comb ct =
   32.21 @@ -173,7 +173,7 @@
   32.22  (*Beta-conversion for cterms, where x is an abstraction. Simply returns the rhs
   32.23    of the meta-equality returned by the beta_conversion rule.*)
   32.24  fun beta_conv x y =
   32.25 -  Thm.dest_arg (cprop_of (Thm.beta_conversion false (Thm.capply x y)));
   32.26 +  Thm.dest_arg (cprop_of (Thm.beta_conversion false (Thm.apply x y)));
   32.27  
   32.28  
   32.29  
   32.30 @@ -673,7 +673,7 @@
   32.31  
   32.32  (* protect *)
   32.33  
   32.34 -val protect = Thm.capply (certify Logic.protectC);
   32.35 +val protect = Thm.apply (certify Logic.protectC);
   32.36  
   32.37  val protectI =
   32.38    store_standard_thm (Binding.conceal (Binding.name "protectI"))
    33.1 --- a/src/Pure/more_thm.ML	Wed Feb 15 22:44:31 2012 +0100
    33.2 +++ b/src/Pure/more_thm.ML	Wed Feb 15 23:19:30 2012 +0100
    33.3 @@ -120,11 +120,11 @@
    33.4    let
    33.5      val cert = Thm.cterm_of (Thm.theory_of_cterm t);
    33.6      val T = #T (Thm.rep_cterm t);
    33.7 -  in Thm.capply (cert (Const ("all", (T --> propT) --> propT))) (Thm.cabs_name (x, t) A) end;
    33.8 +  in Thm.apply (cert (Const ("all", (T --> propT) --> propT))) (Thm.lambda_name (x, t) A) end;
    33.9  
   33.10  fun all t A = all_name ("", t) A;
   33.11  
   33.12 -fun mk_binop c a b = Thm.capply (Thm.capply c a) b;
   33.13 +fun mk_binop c a b = Thm.apply (Thm.apply c a) b;
   33.14  fun dest_binop ct = (Thm.dest_arg1 ct, Thm.dest_arg ct);
   33.15  
   33.16  fun dest_implies ct =
    34.1 --- a/src/Pure/thm.ML	Wed Feb 15 22:44:31 2012 +0100
    34.2 +++ b/src/Pure/thm.ML	Wed Feb 15 23:19:30 2012 +0100
    34.3 @@ -75,9 +75,9 @@
    34.4    val dest_fun2: cterm -> cterm
    34.5    val dest_arg1: cterm -> cterm
    34.6    val dest_abs: string option -> cterm -> cterm * cterm
    34.7 -  val capply: cterm -> cterm -> cterm
    34.8 -  val cabs_name: string * cterm -> cterm -> cterm
    34.9 -  val cabs: cterm -> cterm -> cterm
   34.10 +  val apply: cterm -> cterm -> cterm
   34.11 +  val lambda_name: string * cterm -> cterm -> cterm
   34.12 +  val lambda: cterm -> cterm -> cterm
   34.13    val adjust_maxidx_cterm: int -> cterm -> cterm
   34.14    val incr_indexes_cterm: int -> cterm -> cterm
   34.15    val match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
   34.16 @@ -259,7 +259,7 @@
   34.17  
   34.18  (* constructors *)
   34.19  
   34.20 -fun capply
   34.21 +fun apply
   34.22    (cf as Cterm {t = f, T = Type ("fun", [dty, rty]), maxidx = maxidx1, sorts = sorts1, ...})
   34.23    (cx as Cterm {t = x, T, maxidx = maxidx2, sorts = sorts2, ...}) =
   34.24      if T = dty then
   34.25 @@ -268,10 +268,10 @@
   34.26          T = rty,
   34.27          maxidx = Int.max (maxidx1, maxidx2),
   34.28          sorts = Sorts.union sorts1 sorts2}
   34.29 -      else raise CTERM ("capply: types don't agree", [cf, cx])
   34.30 -  | capply cf cx = raise CTERM ("capply: first arg is not a function", [cf, cx]);
   34.31 +      else raise CTERM ("apply: types don't agree", [cf, cx])
   34.32 +  | apply cf cx = raise CTERM ("apply: first arg is not a function", [cf, cx]);
   34.33  
   34.34 -fun cabs_name
   34.35 +fun lambda_name
   34.36    (x, ct1 as Cterm {t = t1, T = T1, maxidx = maxidx1, sorts = sorts1, ...})
   34.37    (ct2 as Cterm {t = t2, T = T2, maxidx = maxidx2, sorts = sorts2, ...}) =
   34.38      let val t = Term.lambda_name (x, t1) t2 in
   34.39 @@ -281,7 +281,7 @@
   34.40          sorts = Sorts.union sorts1 sorts2}
   34.41      end;
   34.42  
   34.43 -fun cabs t u = cabs_name ("", t) u;
   34.44 +fun lambda t u = lambda_name ("", t) u;
   34.45  
   34.46  
   34.47  (* indexes *)
   34.48 @@ -1548,7 +1548,7 @@
   34.49                if member (op =) ys y
   34.50                then del_clashing true (x :: xs) (x :: ys) ps qs
   34.51                else del_clashing clash xs (y :: ys) ps (p :: qs);
   34.52 -        val al'' = del_clashing false unchanged unchanged al' [];        
   34.53 +        val al'' = del_clashing false unchanged unchanged al' [];
   34.54          fun rename (t as Var ((x, i), T)) =
   34.55                (case AList.lookup (op =) al'' x of
   34.56                   SOME y => Var ((y, i), T)
    35.1 --- a/src/Pure/variable.ML	Wed Feb 15 22:44:31 2012 +0100
    35.2 +++ b/src/Pure/variable.ML	Wed Feb 15 23:19:30 2012 +0100
    35.3 @@ -539,7 +539,7 @@
    35.4    in (((xs ~~ ps), t'), ctxt') end;
    35.5  
    35.6  fun forall_elim_prop t prop =
    35.7 -  Thm.beta_conversion false (Thm.capply (Thm.dest_arg prop) t)
    35.8 +  Thm.beta_conversion false (Thm.apply (Thm.dest_arg prop) t)
    35.9    |> Thm.cprop_of |> Thm.dest_arg;
   35.10  
   35.11  fun focus_cterm goal ctxt =
    36.1 --- a/src/Tools/Code/code_preproc.ML	Wed Feb 15 22:44:31 2012 +0100
    36.2 +++ b/src/Tools/Code/code_preproc.ML	Wed Feb 15 23:19:30 2012 +0100
    36.3 @@ -117,7 +117,7 @@
    36.4        |> Conv.fconv_rule (Conv.arg1_conv (Thm.beta_conversion false));
    36.5    in
    36.6      ct
    36.7 -    |> fold_rev Thm.cabs all_vars
    36.8 +    |> fold_rev Thm.lambda all_vars
    36.9      |> conv
   36.10      |> fold apply_beta all_vars
   36.11    end;