src/HOL/Word/WordArith.thy

--- a/src/HOL/Word/WordArith.thy	Tue Apr 28 15:50:30 2009 +0200
+++ b/src/HOL/Word/WordArith.thy	Tue Apr 28 15:50:30 2009 +0200
@@ -790,15 +790,14 @@
 instance word :: (len) comm_semiring_1 
   by (intro_classes) (simp add: lenw1_zero_neq_one)
 
+instance word :: (len) recpower ..
+
 instance word :: (len) comm_ring_1 ..
 
 instance word :: (len0) comm_semiring_0 ..
 
 instance word :: (len0) order ..
 
-instance word :: (len) recpower
-  by (intro_classes) simp_all
-
 (* note that iszero_def is only for class comm_semiring_1_cancel,
    which requires word length >= 1, ie 'a :: len word *) 
 lemma zero_bintrunc: