--- 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)