diff -r 0dbb30302259 -r 01c09922ce59 src/HOL/Tools/Groebner_Basis/normalizer_data.ML
--- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Mon Jun 11 18:28:15 2007 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Mon Jun 11 18:28:16 2007 +0200
@@ -16,7 +16,7 @@
   val funs: thm -> {is_const: morphism -> cterm -> bool,
     dest_const: morphism -> cterm -> Rat.rat,
     mk_const: morphism -> ctyp -> Rat.rat -> cterm,
-    conv: morphism -> cterm -> thm} -> morphism -> Context.generic -> Context.generic
+    conv: morphism -> Proof.context -> cterm -> thm} -> morphism -> Context.generic -> Context.generic
   val setup: theory -> theory
 end;
 
@@ -33,7 +33,7 @@
  {is_const: cterm -> bool,
   dest_const: cterm -> Rat.rat,
   mk_const: ctyp -> Rat.rat -> cterm,
-  conv: cterm -> thm};
+  conv: Proof.context -> cterm -> thm};
 
 val eq_key = Thm.eq_thm;
 fun eq_data arg = eq_fst eq_key arg;