diff -r 0dbb30302259 -r 01c09922ce59 src/HOL/Tools/Groebner_Basis/normalizer.ML
--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Mon Jun 11 18:28:15 2007 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Mon Jun 11 18:28:16 2007 +0200
@@ -9,7 +9,7 @@
  val mk_cnumeral : integer -> cterm
  val semiring_normalize_conv : Proof.context -> Conv.conv
  val semiring_normalize_tac : Proof.context -> int -> tactic
- val semiring_normalize_wrapper :  NormalizerData.entry -> Conv.conv
+ val semiring_normalize_wrapper :  Proof.context -> NormalizerData.entry -> Conv.conv
  val semiring_normalizers_conv :
      cterm list -> cterm list * thm list -> cterm list * thm list ->
      (cterm -> bool) * Conv.conv * Conv.conv * Conv.conv -> (cterm -> Thm.cterm -> bool) ->
@@ -622,7 +622,7 @@
 val nat_exp_ss = HOL_basic_ss addsimps (nat_number @ nat_arith @ arith_simps @ rel_simps)
                               addsimps [Let_def, if_False, if_True, add_0, add_Suc];
 
-fun semiring_normalize_wrapper ({vars, semiring, ring, idom}, 
+fun semiring_normalize_wrapper ctxt ({vars, semiring, ring, idom}, 
                                      {conv, dest_const, mk_const, is_const}) =
   let
     fun ord t u = Term.term_ord (term_of t, term_of u) = LESS
@@ -631,15 +631,15 @@
       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
-    val dat = (is_const, conv, conv, pow_conv)
+      then_conv conv ctxt
+    val dat = (is_const, conv ctxt, conv ctxt, pow_conv)
     val {main, ...} = semiring_normalizers_conv vars semiring ring dat ord
   in main end;
 
 fun semiring_normalize_conv ctxt tm =
   (case NormalizerData.match ctxt tm of
     NONE => reflexive tm
-  | SOME res => semiring_normalize_wrapper res tm);
+  | SOME res => semiring_normalize_wrapper ctxt res tm);
 
 
 fun semiring_normalize_tac ctxt = SUBGOAL (fn (goal, i) =>