src/HOL/Word/Bit_Int.thy

--- a/src/HOL/Word/Bit_Int.thy	Fri Mar 30 11:52:26 2012 +0200
+++ b/src/HOL/Word/Bit_Int.thy	Fri Mar 30 12:02:23 2012 +0200
@@ -501,8 +501,8 @@
 
 lemma bin_sc_numeral [simp]:
   "bin_sc (numeral k) b w =
-    bin_sc (numeral k - 1) b (bin_rest w) BIT bin_last w"
-  by (subst expand_Suc, rule bin_sc.Suc)
+    bin_sc (pred_numeral k) b (bin_rest w) BIT bin_last w"
+  by (simp add: numeral_eq_Suc)
 
 
 subsection {* Splitting and concatenation *}