# HG changeset patch
# User haftmann
# Date 1273158154 -7200
# Node ID f7329e6734bd80001b4eb36cfeb98f58c1286df2
# Parent  3db7243c24847b0ead1af433f63a9f9b2d01f848
avoid open

diff -r 3db7243c2484 -r f7329e6734bd src/HOL/Tools/Groebner_Basis/normalizer.ML
--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Thu May 06 17:00:46 2010 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Thu May 06 17:02:34 2010 +0200
@@ -170,8 +170,6 @@
   in AList.map_entry Thm.eq_thm key (apsnd (K fns)) data end);
 
 
-open Conv;
-
 (* Very basic stuff for terms *)
 
 fun is_comb ct =
@@ -711,7 +709,7 @@
    let val (l,r) = Thm.dest_comb tm in
         if not (l aconvc neg_tm) then raise CTERM ("polynomial_neg_conv",[tm]) else
         let val th1 = inst_thm [(cx',r)] neg_mul
-            val th2 = transitive th1 (arg1_conv semiring_mul_conv (concl th1))
+            val th2 = transitive th1 (Conv.arg1_conv semiring_mul_conv (concl th1))
         in transitive th2 (polynomial_monomial_mul_conv (concl th2))
         end
    end;
@@ -754,7 +752,7 @@
             then
               let val th1 = combination (Drule.arg_cong_rule opr (polynomial_conv l)) 
                                         (polynomial_conv r)
-                  val th2 = (rewr_conv divide_inverse then_conv polynomial_mul_conv) 
+                  val th2 = (Conv.rewr_conv divide_inverse then_conv polynomial_mul_conv)
                               (Thm.rhs_of th1)
               in transitive th1 th2
               end
@@ -790,7 +788,7 @@
                                      {conv, dest_const, mk_const, is_const}) ord =
   let
     val pow_conv =
-      arg_conv (Simplifier.rewrite nat_exp_ss)
+      Conv.arg_conv (Simplifier.rewrite nat_exp_ss)
       then_conv Simplifier.rewrite
         (HOL_basic_ss addsimps [nth (snd semiring) 31, nth (snd semiring) 34])
       then_conv conv ctxt