--- a/src/HOL/List.thy Mon Nov 18 17:15:01 2013 +0100
+++ b/src/HOL/List.thy Tue Nov 19 17:07:52 2013 +0100
@@ -3075,9 +3075,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)