diff -r 1f9956e0bd89 -r ec39d7e40554 src/HOL/Library/Word.thy
--- a/src/HOL/Library/Word.thy	Thu Jan 24 23:51:22 2008 +0100
+++ b/src/HOL/Library/Word.thy	Fri Jan 25 14:53:52 2008 +0100
@@ -40,11 +40,11 @@
     Zero ("\<zero>")
   | One ("\<one>")
 
-consts
+primrec
   bitval :: "bit => nat"
-primrec
+where
   "bitval \<zero> = 0"
-  "bitval \<one> = 1"
+  | "bitval \<one> = 1"
 
 consts
   bitnot :: "bit => bit"
@@ -1531,7 +1531,7 @@
     show ?thesis
       apply simp
       apply (subst power_Suc [symmetric])
-      apply (simp del: power.simps)
+      apply (simp del: power_int.simps)
       done
   qed
   finally show ?thesis .