diff -r 9999a77590c3 -r 53642251a04f src/HOL/Library/Numeral_Type.thy
--- a/src/HOL/Library/Numeral_Type.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Numeral_Type.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -216,12 +216,6 @@
 apply (simp_all add: Rep_simps zmod_simps ring_simps)
 done
 
-lemma recpower: "OFCLASS('a, recpower_class)"
-apply (intro_classes, unfold definitions)
-apply (simp_all add: Rep_simps zmod_simps add_ac mult_assoc
-                     mod_pos_pos_trivial size1)
-done
-
 end
 
 locale mod_ring = mod_type +
@@ -340,11 +334,11 @@
 apply (rule uminus_bit1_def [unfolded Abs_bit1'_def])
 done
 
-instance bit0 :: (finite) "{comm_ring_1,recpower}"
-  by (rule bit0.comm_ring_1 bit0.recpower)+
+instance bit0 :: (finite) comm_ring_1
+  by (rule bit0.comm_ring_1)+
 
-instance bit1 :: (finite) "{comm_ring_1,recpower}"
-  by (rule bit1.comm_ring_1 bit1.recpower)+
+instance bit1 :: (finite) comm_ring_1
+  by (rule bit1.comm_ring_1)+
 
 instantiation bit0 and bit1 :: (finite) number_ring
 begin