diff -r f2b741473860 -r e08fdd615333 src/HOL/Tools/Function/measure_functions.ML
--- a/src/HOL/Tools/Function/measure_functions.ML	Fri Sep 18 09:07:49 2009 +0200
+++ b/src/HOL/Tools/Function/measure_functions.ML	Fri Sep 18 09:07:50 2009 +0200
@@ -22,7 +22,7 @@
   val description = "Rules that guide the heuristic generation of measure functions"
 );
 
-fun mk_is_measures t = Const (@{const_name "is_measure"}, fastype_of t --> HOLogic.boolT) $ t
+fun mk_is_measures t = Const (@{const_name is_measure}, fastype_of t --> HOLogic.boolT) $ t
 
 fun find_measures ctxt T =
   DEPTH_SOLVE (resolve_tac (Measure_Heuristic_Rules.get ctxt) 1)