diff -r 59c17b0b870d -r 7896762b638b src/HOL/Tools/groebner.ML
--- a/src/HOL/Tools/groebner.ML	Sat Aug 16 14:12:39 2014 +0200
+++ b/src/HOL/Tools/groebner.ML	Sat Aug 16 14:27:41 2014 +0200
@@ -924,7 +924,7 @@
 
 fun presimplify ctxt add_thms del_thms =
   asm_full_simp_tac (put_simpset HOL_basic_ss ctxt
-    addsimps (Algebra_Simplification.get ctxt)
+    addsimps (Named_Theorems.get ctxt @{named_theorems algebra})
     delsimps del_thms addsimps add_thms);
 
 fun ring_tac add_ths del_ths ctxt =