# HG changeset patch
# User krauss
# Date 1184675880 -7200
# Node ID 41014a878a7def80d9e322ed8e1f35c3cc9fb4b9
# Parent  a8a3962f8eebd87c9dbd2b2715ef3e9f129b1214
reverted fun->recdef, since there are problems with induction rule

diff -r a8a3962f8eeb -r 41014a878a7d src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Tue Jul 17 13:19:47 2007 +0200
+++ b/src/HOL/Library/Word.thy	Tue Jul 17 14:38:00 2007 +0200
@@ -322,11 +322,11 @@
 lemma norm_unsigned_idem [simp]: "norm_unsigned (norm_unsigned w) = norm_unsigned w"
   by (rule bit_list_induct [of _ w],simp_all)
 
-fun
+consts
   nat_to_bv_helper :: "nat => bit list => bit list"
-where (*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))"
+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)))"
 
 definition
   nat_to_bv :: "nat => bit list" where