--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML Thu May 06 16:40:02 2010 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML Thu May 06 16:41:14 2010 +0200
@@ -7,7 +7,7 @@
signature NORMALIZER =
sig
type entry
- val get: Proof.context -> simpset * (thm * entry) list
+ val get: Proof.context -> (thm * entry) list
val match: Proof.context -> cterm -> entry option
val del: attribute
val add: {semiring: cterm list * thm list, ring: cterm list * thm list, field: cterm list * thm list, idom: thm list, ideal: thm list}
@@ -62,7 +62,7 @@
(merge_ss (ss, ss'), AList.merge eq_key (K true) (e, e'));
);
-val get = Data.get o Context.Proof;
+val get = snd o Data.get o Context.Proof;
(* match data *)