--- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Sat Jul 28 20:40:22 2007 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML Sat Jul 28 20:40:24 2007 +0200
@@ -16,8 +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 -> Proof.context -> cterm -> thm} ->
- morphism -> Context.generic -> Context.generic
+ conv: morphism -> Proof.context -> cterm -> thm} -> declaration
val setup: theory -> theory
end;