removed former algebra presimpset from accessor
authorhaftmann
Thu, 06 May 2010 16:50:26 +0200
changeset 36704 9dd2fe596ace
parent 36703 6e870d7f32e5
child 36705 4a7709f041a8
removed former algebra presimpset from accessor
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 *)