diff -r 57def0b39696 -r 3c5d3d286055 src/HOL/Tools/Function/measure_functions.ML
--- a/src/HOL/Tools/Function/measure_functions.ML	Fri Oct 28 23:16:50 2011 +0200
+++ b/src/HOL/Tools/Function/measure_functions.ML	Fri Oct 28 23:41:16 2011 +0200
@@ -18,7 +18,7 @@
 (** User-declared size functions **)
 structure Measure_Heuristic_Rules = Named_Thms
 (
-  val name = "measure_function"
+  val name = @{binding measure_function}
   val description =
     "rules that guide the heuristic generation of measure functions"
 );