--- 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. *}