src/HOL/Library/Code_Index.thy

--- a/src/HOL/Library/Code_Index.thy	Thu Aug 28 15:33:33 2008 +0200
+++ b/src/HOL/Library/Code_Index.thy	Thu Aug 28 17:54:18 2008 +0200
@@ -232,6 +232,10 @@
   by (simp add: nat_of_index_aux_def)
 
 
+text {* Measure function (for termination proofs) *}
+
+lemma [measure_function]: "is_measure nat_of_index" by (rule is_measure_trivial)
+
 subsection {* ML interface *}
 
 ML {*