1.1 --- a/src/HOL/Groebner_Basis.thy	Sat Aug 16 14:12:39 2014 +0200
     1.2 +++ b/src/HOL/Groebner_Basis.thy	Sat Aug 16 14:27:41 2014 +0200
     1.3 @@ -33,16 +33,7 @@
     1.4      "\<not> P \<Longrightarrow> (P \<equiv> False)"
     1.5    by auto
     1.6  
     1.7 -ML {*
     1.8 -structure Algebra_Simplification = Named_Thms
     1.9 -(
    1.10 -  val name = @{binding algebra}
    1.11 -  val description = "pre-simplification rules for algebraic methods"
    1.12 -)
    1.13 -*}
    1.14 -
    1.15 -setup Algebra_Simplification.setup
    1.16 -
    1.17 +named_theorems algebra "pre-simplification rules for algebraic methods"
    1.18  ML_file "Tools/groebner.ML"
    1.19  
    1.20  method_setup algebra = {*