# HG changeset patch
# User wenzelm
# Date 1408192061 -7200
# Node ID 7896762b638be63489dedfba34a6705f9a4711b6
# Parent  59c17b0b870d3b45cb4d85a02f17e552f9ebb479
updated to named_theorems;

diff -r 59c17b0b870d -r 7896762b638b src/HOL/Groebner_Basis.thy
--- 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 = {*
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 =