1.1 --- a/src/HOL/Word/Word.thy	Tue Dec 27 15:38:45 2011 +0100
     1.2 +++ b/src/HOL/Word/Word.thy	Tue Dec 27 18:26:15 2011 +0100
     1.3 @@ -249,16 +249,10 @@
     1.4    "(word_of_int a) - word_of_int b = word_of_int (a - b)"
     1.5    by (simp add: word_sub_wi arths)
     1.6  
     1.7 -lemmas new_word_of_int_homs = 
     1.8 -  word_of_int_sub_hom wi_homs word_0_wi word_1_wi 
     1.9 -
    1.10 -lemmas new_word_of_int_hom_syms = new_word_of_int_homs [symmetric]
    1.11 -
    1.12 -lemmas word_of_int_hom_syms =
    1.13 -  new_word_of_int_hom_syms (* FIXME: duplicate *)
    1.14 -
    1.15  lemmas word_of_int_homs =
    1.16 -  new_word_of_int_homs (* FIXME: duplicate *)
    1.17 +  word_of_int_sub_hom wi_homs word_0_wi word_1_wi
    1.18 +
    1.19 +lemmas word_of_int_hom_syms = word_of_int_homs [symmetric]
    1.20  
    1.21  (* FIXME: provide only one copy of these theorems! *)
    1.22  lemmas word_of_int_add_hom = wi_hom_add
    1.23 @@ -1204,7 +1198,7 @@
    1.24    by (rule word_uint.Abs_cases [of b],
    1.25        rule word_uint.Abs_cases [of a],
    1.26        simp add: add_commute mult_commute 
    1.27 -                ring_distribs new_word_of_int_homs
    1.28 +                ring_distribs word_of_int_homs
    1.29             del: word_of_int_0 word_of_int_1)+
    1.30  
    1.31  lemma uint_cong: "x = y \<Longrightarrow> uint x = uint y"
    1.32 @@ -1237,7 +1231,7 @@
    1.33    "word_succ (number_of bin) = number_of (Int.succ bin) & 
    1.34      word_pred (number_of bin) = number_of (Int.pred bin)"
    1.35    unfolding word_number_of_def Int.succ_def Int.pred_def
    1.36 -  by (simp add: new_word_of_int_homs)
    1.37 +  by (simp add: word_of_int_homs)
    1.38  
    1.39  lemma word_sp_01 [simp] : 
    1.40    "word_succ -1 = 0 & word_succ 0 = 1 & word_pred 0 = -1 & word_pred 1 = 0"
    1.41 @@ -3152,7 +3146,7 @@
    1.42    "word_succ (a AND mask n) AND mask n = word_succ a AND mask n"
    1.43    "word_pred (a AND mask n) AND mask n = word_pred a AND mask n"
    1.44    using word_of_int_Ex [where x=a] word_of_int_Ex [where x=b]
    1.45 -  by (auto simp: and_mask_wi bintr_ariths bintr_arith1s new_word_of_int_homs)
    1.46 +  by (auto simp: and_mask_wi bintr_ariths bintr_arith1s word_of_int_homs)
    1.47  
    1.48  lemma mask_power_eq:
    1.49    "(x AND mask n) ^ k AND mask n = x ^ k AND mask n"
    1.50 @@ -3448,7 +3442,7 @@
    1.51    "(of_bl (xs @ ys) :: 'a :: len word) = of_bl xs * 2^(length ys) + of_bl ys"
    1.52    apply (unfold of_bl_def)
    1.53    apply (simp add: bl_to_bin_app_cat bin_cat_num)
    1.54 -  apply (simp add: word_of_int_power_hom [symmetric] new_word_of_int_hom_syms)
    1.55 +  apply (simp add: word_of_int_power_hom [symmetric] word_of_int_hom_syms)
    1.56    done
    1.57  
    1.58  lemma of_bl_False [simp]: