1.1 --- a/src/HOL/Word/Bool_List_Representation.thy	Fri Feb 24 16:55:29 2012 +0100
     1.2 +++ b/src/HOL/Word/Bool_List_Representation.thy	Fri Feb 24 16:59:20 2012 +0100
     1.3 @@ -790,7 +790,7 @@
     1.4    apply (case_tac binb rule: bin_exhaust)
     1.5    apply (case_tac b)
     1.6     apply (case_tac [!] "ba")
     1.7 -     apply (auto simp: rbl_succ succ_def bin_to_bl_aux_alt Let_def add_ac)
     1.8 +     apply (auto simp: rbl_succ bin_to_bl_aux_alt Let_def add_ac)
     1.9    done
    1.10  
    1.11  lemma rbl_add_app2: