src/HOL/Tools/Function/function_common.ML

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