diff -r 83a5160e6b4d -r 9f9e85264e4d src/HOL/Word/Bit_Int.thy
--- a/src/HOL/Word/Bit_Int.thy	Thu Feb 23 12:45:00 2012 +0100
+++ b/src/HOL/Word/Bit_Int.thy	Thu Feb 23 13:16:18 2012 +0100
@@ -279,14 +279,15 @@
   done
 
 lemma le_int_or:
-  "bin_sign (y::int) = Int.Pls ==> x <= x OR y"
+  "bin_sign (y::int) = 0 ==> x <= x OR y"
   apply (induct y arbitrary: x rule: bin_induct)
     apply clarsimp
+   apply (simp only: Min_def)
    apply clarsimp
   apply (case_tac x rule: bin_exhaust)
   apply (case_tac b)
    apply (case_tac [!] bit)
-     apply (auto simp: less_eq_int_code BIT_simps)
+     apply (auto simp: le_Bits)
   done
 
 lemmas int_and_le =