1.1 --- a/src/HOL/Tools/Function/function_common.ML	Fri Oct 28 23:16:50 2011 +0200
     1.2 +++ b/src/HOL/Tools/Function/function_common.ML	Fri Oct 28 23:41:16 2011 +0200
     1.3 @@ -161,7 +161,7 @@
     1.4  
     1.5  structure Termination_Simps = Named_Thms
     1.6  (
     1.7 -  val name = "termination_simp"
     1.8 +  val name = @{binding termination_simp}
     1.9    val description = "simplification rules for termination proofs"
    1.10  )
    1.11