# HG changeset patch
# User haftmann
# Date 1273157426 -7200
# Node ID 9dd2fe596ace355b6a38fcf46546fe0f1da4dc94
# Parent  6e870d7f32e5f7e119ffa77d0832556c0dc39d4e
removed former algebra presimpset from accessor

diff -r 6e870d7f32e5 -r 9dd2fe596ace src/HOL/Tools/Groebner_Basis/normalizer.ML
--- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Thu May 06 16:41:14 2010 +0200
+++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Thu May 06 16:50:26 2010 +0200
@@ -97,7 +97,7 @@
     fun match_struct (_,
         entry as ({semiring = (sr_ops, _), ring = (r_ops, _), field = (f_ops, _), ...}, _): entry) =
       get_first (match_inst entry) (sr_ops @ r_ops @ f_ops);
-  in get_first match_struct (snd (get ctxt)) end;
+  in get_first match_struct (get ctxt) end;
 
 
 (* logical content *)