--- a/src/HOL/Word/Bits_Int.thy Sun Sep 21 16:56:06 2014 +0200
+++ b/src/HOL/Word/Bits_Int.thy Sun Sep 21 16:56:11 2014 +0200
@@ -462,7 +462,7 @@
lemma bin_sc_FP [simp]: "bin_sc n False 0 = 0"
by (induct n) auto
-lemma bin_sc_TM [simp]: "bin_sc n True -1 = -1"
+lemma bin_sc_TM [simp]: "bin_sc n True (- 1) = - 1"
by (induct n) auto
lemmas bin_sc_simps = bin_sc.Z bin_sc.Suc bin_sc_TM bin_sc_FP
@@ -583,7 +583,7 @@
by (induct n) auto
lemma bin_split_minus1 [simp]:
- "bin_split n -1 = (-1, bintrunc n -1)"
+ "bin_split n (- 1) = (- 1, bintrunc n (- 1))"
by (induct n) auto
lemma bin_split_trunc: