diff -r 27f3c10b0b50 -r 4cf66f21b764 src/HOL/Word/Bit_Comparison.thy
--- a/src/HOL/Word/Bit_Comparison.thy	Mon Dec 07 10:23:50 2015 +0100
+++ b/src/HOL/Word/Bit_Comparison.thy	Mon Dec 07 10:38:04 2015 +0100
@@ -137,7 +137,7 @@
       with 3 have "bin BIT bit = 0" by simp
       then have "bin = 0" and "\<not> bit"
         by (auto simp add: Bit_def split: if_splits) arith
-      then show ?thesis using 0 1 `y < 2 ^ n`
+      then show ?thesis using 0 1 \<open>y < 2 ^ n\<close>
         by simp
     next
       case (Suc m)
@@ -170,7 +170,7 @@
       with 3 have "bin BIT bit = 0" by simp
       then have "bin = 0" and "\<not> bit"
         by (auto simp add: Bit_def split: if_splits) arith
-      then show ?thesis using 0 1 `y < 2 ^ n`
+      then show ?thesis using 0 1 \<open>y < 2 ^ n\<close>
         by simp
     next
       case (Suc m)