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 =