src/HOL/List.ML

--- a/src/HOL/List.ML	Thu Mar 06 16:04:23 1997 +0100
+++ b/src/HOL/List.ML	Thu Mar 06 16:05:32 1997 +0100
@@ -288,11 +288,6 @@
 
 (** nth **)
 
-val [nth_0,nth_Suc] = nat_recs nth_def; 
-store_thm("nth_0",nth_0);
-store_thm("nth_Suc",nth_Suc);
-Addsimps [nth_0,nth_Suc];
-
 goal List.thy
   "!xs. nth n (xs@ys) = \
 \          (if n < length xs then nth n xs else nth (n - length xs) ys)";