1.1 --- a/src/HOL/List.thy	Tue Nov 19 01:30:14 2013 +0100
     1.2 +++ b/src/HOL/List.thy	Tue Nov 19 10:05:53 2013 +0100
     1.3 @@ -3072,9 +3072,9 @@
     1.4  
     1.5  lemmas upto_rec_numeral [simp] =
     1.6    upto.simps[of "numeral m" "numeral n"]
     1.7 -  upto.simps[of "numeral m" "neg_numeral n"]
     1.8 -  upto.simps[of "neg_numeral m" "numeral n"]
     1.9 -  upto.simps[of "neg_numeral m" "neg_numeral n"] for m n
    1.10 +  upto.simps[of "numeral m" "- numeral n"]
    1.11 +  upto.simps[of "- numeral m" "numeral n"]
    1.12 +  upto.simps[of "- numeral m" "- numeral n"] for m n
    1.13  
    1.14  lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
    1.15  by(simp add: upto.simps)