--- a/src/HOL/Groebner_Basis.thy Sat Aug 16 14:12:39 2014 +0200
+++ b/src/HOL/Groebner_Basis.thy Sat Aug 16 14:27:41 2014 +0200
@@ -33,16 +33,7 @@
"\<not> P \<Longrightarrow> (P \<equiv> False)"
by auto
-ML {*
-structure Algebra_Simplification = Named_Thms
-(
- val name = @{binding algebra}
- val description = "pre-simplification rules for algebraic methods"
-)
-*}
-
-setup Algebra_Simplification.setup
-
+named_theorems algebra "pre-simplification rules for algebraic methods"
ML_file "Tools/groebner.ML"
method_setup algebra = {*
--- 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 =