--- a/src/HOL/List.thy Tue Nov 19 01:30:14 2013 +0100
+++ b/src/HOL/List.thy Tue Nov 19 10:05:53 2013 +0100
@@ -3072,9 +3072,9 @@
lemmas upto_rec_numeral [simp] =
upto.simps[of "numeral m" "numeral n"]
- upto.simps[of "numeral m" "neg_numeral n"]
- upto.simps[of "neg_numeral m" "numeral n"]
- upto.simps[of "neg_numeral m" "neg_numeral n"] for m n
+ upto.simps[of "numeral m" "- numeral n"]
+ upto.simps[of "- numeral m" "numeral n"]
+ upto.simps[of "- numeral m" "- numeral n"] for m n
lemma upto_empty[simp]: "j < i \<Longrightarrow> [i..j] = []"
by(simp add: upto.simps)