src/HOL/Tools/Function/function_common.ML

 
 (* Simp rules for termination proofs *)
 
 structure Termination_Simps = Named_Thms
 (
-  val name = "termination_simp"
+  val name = @{binding termination_simp}
   val description = "simplification rules for termination proofs"
 )
 
 
 (* Default Termination Prover *)