src/HOL/List.thy

--- a/src/HOL/List.thy	Fri Feb 28 22:00:13 2014 +0100
+++ b/src/HOL/List.thy	Fri Feb 28 17:54:52 2014 +0100
@@ -3117,7 +3117,7 @@
 proof(induct i j rule:upto.induct)
   case (1 i j)
   from this show ?case
-    unfolding upto.simps[of i j] simp_from_to[of i j] by auto
+    unfolding upto.simps[of i j] by auto
 qed
 
 text{* Tail recursive version for code generation: *}