src/HOL/Groebner_Basis.thy
changeset 45294 3c5d3d286055
parent 36752 cf558aeb35b0
child 47142 d64fa2ca54b8
--- a/src/HOL/Groebner_Basis.thy	Fri Oct 28 23:16:50 2011 +0200
+++ b/src/HOL/Groebner_Basis.thy	Fri Oct 28 23:41:16 2011 +0200
@@ -32,8 +32,9 @@
   by auto
 
 ML {*
-structure Algebra_Simplification = Named_Thms(
-  val name = "algebra"
+structure Algebra_Simplification = Named_Thms
+(
+  val name = @{binding algebra}
   val description = "pre-simplification rules for algebraic methods"
 )
 *}