eliminated alias;
authorwenzelm
Fri Jan 07 23:02:12 2011 +0100 (2011-01-07)
changeset 414541db1b47cec3d
parent 41453 c03593812297
child 41455 d3be2a414d15
eliminated alias;
src/HOL/Tools/groebner.ML
     1.1 --- a/src/HOL/Tools/groebner.ML	Fri Jan 07 22:44:07 2011 +0100
     1.2 +++ b/src/HOL/Tools/groebner.ML	Fri Jan 07 23:02:12 2011 +0100
     1.3 @@ -397,7 +397,6 @@
     1.4  val notnotD = @{thm notnotD};
     1.5  fun mk_binop ct x y = Thm.capply (Thm.capply ct x) y
     1.6  
     1.7 -val mk_comb = Thm.capply;
     1.8  fun is_neg t =
     1.9      case term_of t of
    1.10        (Const(@{const_name Not},_)$p) => true
    1.11 @@ -452,10 +451,10 @@
    1.12  val cTrp = @{cterm "Trueprop"};
    1.13  val cConj = @{cterm HOL.conj};
    1.14  val (cNot,false_tm) = (@{cterm "Not"}, @{cterm "False"});
    1.15 -val assume_Trueprop = mk_comb cTrp #> Thm.assume;
    1.16 +val assume_Trueprop = Thm.capply cTrp #> Thm.assume;
    1.17  val list_mk_conj = list_mk_binop cConj;
    1.18  val conjs = list_dest_binop cConj;
    1.19 -val mk_neg = mk_comb cNot;
    1.20 +val mk_neg = Thm.capply cNot;
    1.21  
    1.22  fun striplist dest =
    1.23   let
    1.24 @@ -608,7 +607,7 @@
    1.25         else raise CTERM ("ring_dest_neg", [t])
    1.26      end
    1.27  
    1.28 - val ring_mk_neg = fn tm => mk_comb (ring_neg_tm) (tm);
    1.29 + val ring_mk_neg = fn tm => Thm.capply (ring_neg_tm) (tm);
    1.30   fun field_dest_inv t =
    1.31      let val (l,r) = Thm.dest_comb t in
    1.32          if Term.could_unify(term_of l, term_of field_inv_tm) then r
    1.33 @@ -728,7 +727,7 @@
    1.34            ((Conv.arg_conv #> Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) th1
    1.35        val conc = th2 |> concl |> Thm.dest_arg
    1.36        val (l,r) = conc |> dest_eq
    1.37 -    in Thm.implies_intr (mk_comb cTrp tm)
    1.38 +    in Thm.implies_intr (Thm.capply cTrp tm)
    1.39                      (Thm.equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th2))
    1.40                             (Thm.reflexive l |> mk_object_eq))
    1.41      end
    1.42 @@ -759,7 +758,7 @@
    1.43      fun thm_fn pols =
    1.44          if null pols then Thm.reflexive(mk_const rat_0) else
    1.45          end_itlist mk_add
    1.46 -            (map (fn (i,p) => Drule.arg_cong_rule (mk_comb ring_mul_tm p)
    1.47 +            (map (fn (i,p) => Drule.arg_cong_rule (Thm.capply ring_mul_tm p)
    1.48                (nth eths i |> mk_meta_eq)) pols)
    1.49      val th1 = thm_fn herts_pos
    1.50      val th2 = thm_fn herts_neg
    1.51 @@ -768,7 +767,7 @@
    1.52        Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv o Conv.binop_conv) ring_normalize_conv)
    1.53          (neq_rule l th3)
    1.54      val (l,r) = dest_eq(Thm.dest_arg(concl th4))
    1.55 -   in Thm.implies_intr (mk_comb cTrp tm)
    1.56 +   in Thm.implies_intr (Thm.capply cTrp tm)
    1.57                          (Thm.equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th4))
    1.58                     (Thm.reflexive l |> mk_object_eq))
    1.59     end
    1.60 @@ -777,7 +776,7 @@
    1.61  fun ring tm =
    1.62   let
    1.63    fun mk_forall x p =
    1.64 -    mk_comb
    1.65 +    Thm.capply
    1.66        (Drule.cterm_rule (instantiate' [SOME (ctyp_of_term x)] [])
    1.67          @{cpat "All:: (?'a => bool) => _"}) (Thm.cabs x p)
    1.68    val avs = Thm.add_cterm_frees tm []