src/HOL/Word/Word.thy

--- a/src/HOL/Word/Word.thy	Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Word/Word.thy	Tue Sep 07 10:05:19 2010 +0200
@@ -4695,7 +4695,7 @@
 apply simp
 apply (rule_tac t="\<lambda>a. x (1 + (n - m + a))" and s="\<lambda>a. x (1 + (n - m) + a)"
        in subst)
- apply (clarsimp simp add: expand_fun_eq)
+ apply (clarsimp simp add: ext_iff)
  apply (rule_tac t="(1 + (n - m + xb))" and s="1 + (n - m) + xb" in subst)
   apply simp
  apply (rule refl)