--- 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 = {*