tuned setup for the fields instantiation for Groebner Bases;

--- a/src/HOL/NatSimprocs.thy	Mon Jun 11 18:26:44 2007 +0200
+++ b/src/HOL/NatSimprocs.thy	Mon Jun 11 18:28:15 2007 +0200
@@ -425,7 +425,9 @@
  val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
  val add_num_frac = mk_meta_eq @{thm "add_num_frac"}
 
- fun prove_nz ss T t = 
+ fun prove_nz ctxt =
+  let val ss = local_simpset_of ctxt 
+  in fn T => fn t => 
     let 
       val z = instantiate_cterm ([(zT,T)],[]) zr 
       val eq = instantiate_cterm ([(eqT,T)],[]) geq
@@ -434,20 +436,21 @@
                   (Thm.capply (Thm.capply eq t) z)))
     in equal_elim (symmetric th) TrueI
     end
+  end
 
- fun proc phi ss ct = 
+ fun proc ctxt phi ss ct = 
   let 
     val ((x,y),(w,z)) = 
          (Thm.dest_binop #> (fn (a,b) => (Thm.dest_binop a, Thm.dest_binop b))) ct
     val _ = map (HOLogic.dest_number o term_of) [x,y,z,w] 
     val T = ctyp_of_term x
-    val [y_nz, z_nz] = map (prove_nz ss T) [y, z]
+    val [y_nz, z_nz] = map (prove_nz ctxt T) [y, z]
     val th = instantiate' [SOME T] (map SOME [y,z,x,w]) add_frac_eq
   in SOME (implies_elim (implies_elim th y_nz) z_nz)
   end
   handle CTERM _ => NONE | TERM _ => NONE | THM _ => NONE
 
- fun proc2 phi ss ct = 
+ fun proc2 ctxt phi ss ct = 
   let 
     val (l,r) = Thm.dest_binop ct
     val T = ctyp_of_term l
@@ -455,13 +458,13 @@
       (Const(@{const_name "HOL.divide"},_)$_$_, _) => 
         let val (x,y) = Thm.dest_binop l val z = r
             val _ = map (HOLogic.dest_number o term_of) [x,y,z]
-            val ynz = prove_nz ss T y
+            val ynz = prove_nz ctxt T y
         in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,x,z]) add_frac_num) ynz)
         end
      | (_, Const (@{const_name "HOL.divide"},_)$_$_) => 
         let val (x,y) = Thm.dest_binop r val z = l
             val _ = map (HOLogic.dest_number o term_of) [x,y,z]
-            val ynz = prove_nz ss T y
+            val ynz = prove_nz ctxt T y
         in SOME (implies_elim (instantiate' [SOME T] (map SOME [y,z,x]) add_num_frac) ynz)
         end
      | _ => NONE)
@@ -520,15 +523,15 @@
   | _ => NONE)
   handle TERM _ => NONE | CTERM _ => NONE | THM _ => NONE
 
-val add_frac_frac_simproc = 
+fun add_frac_frac_simproc ctxt = 
        make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + (?w::?'a::field)/?z"}], 
                      name = "add_frac_frac_simproc",
-                     proc = proc, identifier = []}
+                     proc = proc ctxt, identifier = []}
 
-val add_frac_num_simproc = 
+fun add_frac_num_simproc ctxt = 
        make_simproc {lhss = [@{cpat "(?x::?'a::field)/?y + ?z"}, @{cpat "?z + (?x::?'a::field)/?y"}], 
                      name = "add_frac_num_simproc",
-                     proc = proc2, identifier = []}
+                     proc = proc2 ctxt, identifier = []}
 
 val ord_frac_simproc = 
   make_simproc 
@@ -558,14 +561,15 @@
            @{thm "diff_def"}, @{thm "minus_divide_left"}, 
            @{thm "Numeral1_eq1_nat"}, @{thm "add_divide_distrib"} RS sym]
 
-val ss = HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"} 
-                 addsimps ths addsimps comp_arith addsimps simp_thms
-                 addsimprocs field_cancel_numeral_factors
-                 addsimprocs [add_frac_frac_simproc, add_frac_num_simproc,
-                              ord_frac_simproc]
-                 addcongs [@{thm "if_weak_cong"}]
 
-val comp_conv = Simplifier.rewrite ss
+fun comp_conv ctxt = Simplifier.rewrite  
+(HOL_basic_ss addsimps @{thms "Groebner_Basis.comp_arith"} 
+              addsimps ths addsimps comp_arith addsimps simp_thms
+              addsimprocs field_cancel_numeral_factors
+               addsimprocs [add_frac_frac_simproc ctxt, add_frac_num_simproc ctxt,
+                            ord_frac_simproc]
+                addcongs [@{thm "if_weak_cong"}])
+
 
 fun numeral_is_const ct = 
   case term_of ct of