1.1 --- a/src/HOL/Tools/Function/measure_functions.ML	Thu Aug 26 20:42:09 2010 +0200
     1.2 +++ b/src/HOL/Tools/Function/measure_functions.ML	Thu Aug 26 21:04:22 2010 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4  (
     1.5    val name = "measure_function"
     1.6    val description =
     1.7 -    "Rules that guide the heuristic generation of measure functions"
     1.8 +    "rules that guide the heuristic generation of measure functions"
     1.9  );
    1.10  
    1.11  fun mk_is_measure t =