1.1 --- a/src/HOL/Groups.thy	Fri Oct 28 23:16:50 2011 +0200
     1.2 +++ b/src/HOL/Groups.thy	Fri Oct 28 23:41:16 2011 +0200
     1.3 @@ -12,8 +12,9 @@
     1.4  subsection {* Fact collections *}
     1.5  
     1.6  ML {*
     1.7 -structure Ac_Simps = Named_Thms(
     1.8 -  val name = "ac_simps"
     1.9 +structure Ac_Simps = Named_Thms
    1.10 +(
    1.11 +  val name = @{binding ac_simps}
    1.12    val description = "associativity and commutativity simplification rules"
    1.13  )
    1.14  *}
    1.15 @@ -30,8 +31,9 @@
    1.16  inverses or division. This is catered for by @{text field_simps}. *}
    1.17  
    1.18  ML {*
    1.19 -structure Algebra_Simps = Named_Thms(
    1.20 -  val name = "algebra_simps"
    1.21 +structure Algebra_Simps = Named_Thms
    1.22 +(
    1.23 +  val name = @{binding algebra_simps}
    1.24    val description = "algebra simplification rules"
    1.25  )
    1.26  *}
    1.27 @@ -44,8 +46,9 @@
    1.28  more benign @{text algebra_simps}. *}
    1.29  
    1.30  ML {*
    1.31 -structure Field_Simps = Named_Thms(
    1.32 -  val name = "field_simps"
    1.33 +structure Field_Simps = Named_Thms
    1.34 +(
    1.35 +  val name = @{binding field_simps}
    1.36    val description = "algebra simplification rules for fields"
    1.37  )
    1.38  *}