1.1 --- a/src/HOL/Tools/Function/measure_functions.ML	Fri Oct 28 23:16:50 2011 +0200
     1.2 +++ b/src/HOL/Tools/Function/measure_functions.ML	Fri Oct 28 23:41:16 2011 +0200
     1.3 @@ -18,7 +18,7 @@
     1.4  (** User-declared size functions **)
     1.5  structure Measure_Heuristic_Rules = Named_Thms
     1.6  (
     1.7 -  val name = "measure_function"
     1.8 +  val name = @{binding measure_function}
     1.9    val description =
    1.10      "rules that guide the heuristic generation of measure functions"
    1.11  );