src/HOL/Tools/groebner.ML
changeset 57951 7896762b638b
parent 54742 7a86358a3c0b
child 59582 0fbed69ff081
--- 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 =