--- a/src/HOL/Library/Word.thy Mon Mar 01 18:49:55 2010 +0100
+++ b/src/HOL/Library/Word.thy Tue Mar 02 12:26:50 2010 +0100
@@ -311,11 +311,11 @@
lemma norm_unsigned_idem [simp]: "norm_unsigned (norm_unsigned w) = norm_unsigned w"
by (rule bit_list_induct [of _ w],simp_all)
-consts
+fun
nat_to_bv_helper :: "nat => bit list => bit list"
-recdef nat_to_bv_helper "measure (\<lambda>n. n)"
- "nat_to_bv_helper n = (%bs. (if n = 0 then bs
- else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then \<zero> else \<one>)#bs)))"
+where
+ "nat_to_bv_helper n bs = (if n = 0 then bs
+ else nat_to_bv_helper (n div 2) ((if n mod 2 = 0 then \<zero> else \<one>)#bs))"
definition
nat_to_bv :: "nat => bit list" where