# HG changeset patch
# User wenzelm
# Date 1294437732 -3600
# Node ID 1db1b47cec3d01fbfb9bcbb5c5b27dab0642a514
# Parent  c035938122970948e0d8a74f4e68a15c543487a9
eliminated alias;

diff -r c03593812297 -r 1db1b47cec3d src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Fri Jan 07 22:44:07 2011 +0100
+++ b/src/HOL/Tools/groebner.ML	Fri Jan 07 23:02:12 2011 +0100
@@ -397,7 +397,6 @@
 val notnotD = @{thm notnotD};
 fun mk_binop ct x y = Thm.capply (Thm.capply ct x) y
 
-val mk_comb = Thm.capply;
 fun is_neg t =
     case term_of t of
       (Const(@{const_name Not},_)$p) => true
@@ -452,10 +451,10 @@
 val cTrp = @{cterm "Trueprop"};
 val cConj = @{cterm HOL.conj};
 val (cNot,false_tm) = (@{cterm "Not"}, @{cterm "False"});
-val assume_Trueprop = mk_comb cTrp #> Thm.assume;
+val assume_Trueprop = Thm.capply cTrp #> Thm.assume;
 val list_mk_conj = list_mk_binop cConj;
 val conjs = list_dest_binop cConj;
-val mk_neg = mk_comb cNot;
+val mk_neg = Thm.capply cNot;
 
 fun striplist dest =
  let
@@ -608,7 +607,7 @@
        else raise CTERM ("ring_dest_neg", [t])
     end
 
- val ring_mk_neg = fn tm => mk_comb (ring_neg_tm) (tm);
+ val ring_mk_neg = fn tm => Thm.capply (ring_neg_tm) (tm);
  fun field_dest_inv t =
     let val (l,r) = Thm.dest_comb t in
         if Term.could_unify(term_of l, term_of field_inv_tm) then r
@@ -728,7 +727,7 @@
           ((Conv.arg_conv #> Conv.arg_conv) (Conv.binop_conv ring_normalize_conv)) th1
       val conc = th2 |> concl |> Thm.dest_arg
       val (l,r) = conc |> dest_eq
-    in Thm.implies_intr (mk_comb cTrp tm)
+    in Thm.implies_intr (Thm.capply cTrp tm)
                     (Thm.equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th2))
                            (Thm.reflexive l |> mk_object_eq))
     end
@@ -759,7 +758,7 @@
     fun thm_fn pols =
         if null pols then Thm.reflexive(mk_const rat_0) else
         end_itlist mk_add
-            (map (fn (i,p) => Drule.arg_cong_rule (mk_comb ring_mul_tm p)
+            (map (fn (i,p) => Drule.arg_cong_rule (Thm.capply ring_mul_tm p)
               (nth eths i |> mk_meta_eq)) pols)
     val th1 = thm_fn herts_pos
     val th2 = thm_fn herts_neg
@@ -768,7 +767,7 @@
       Conv.fconv_rule ((Conv.arg_conv o Conv.arg_conv o Conv.binop_conv) ring_normalize_conv)
         (neq_rule l th3)
     val (l,r) = dest_eq(Thm.dest_arg(concl th4))
-   in Thm.implies_intr (mk_comb cTrp tm)
+   in Thm.implies_intr (Thm.capply cTrp tm)
                         (Thm.equal_elim (Drule.arg_cong_rule cTrp (eqF_intr th4))
                    (Thm.reflexive l |> mk_object_eq))
    end
@@ -777,7 +776,7 @@
 fun ring tm =
  let
   fun mk_forall x p =
-    mk_comb
+    Thm.capply
       (Drule.cterm_rule (instantiate' [SOME (ctyp_of_term x)] [])
         @{cpat "All:: (?'a => bool) => _"}) (Thm.cabs x p)
   val avs = Thm.add_cterm_frees tm []