# HG changeset patch
# User haftmann
# Date 1273156874 -7200
# Node ID 6e870d7f32e5f7e119ffa77d0832556c0dc39d4e
# Parent  b455ebd637999ae73120a0a6a147bd12df8fa7dc
removed former algebra presimpset from signature

diff -r b455ebd63799 -r 6e870d7f32e5 src/HOL/Tools/Groebner_Basis/normalizer.ML
--- 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 *)