diff -r 83b0f75810f0 -r d78659d1723e src/HOL/ex/ThreeDivides.thy
--- a/src/HOL/ex/ThreeDivides.thy	Mon Mar 01 16:42:45 2010 +0100
+++ b/src/HOL/ex/ThreeDivides.thy	Mon Mar 01 17:05:57 2010 +0100
@@ -149,10 +149,10 @@
 The function @{text "nlen"} returns the number of digits in a natural
 number n. *}
 
-consts nlen :: "nat \<Rightarrow> nat"
-recdef nlen "measure id"
+fun nlen :: "nat \<Rightarrow> nat"
+where
   "nlen 0 = 0"
-  "nlen x = 1 + nlen (x div 10)"
+| "nlen x = 1 + nlen (x div 10)"
 
 text {* The function @{text "sumdig"} returns the sum of all digits in
 some number n. *}