renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
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;