src/HOL/List.thy

--- a/src/HOL/List.thy	Thu Mar 06 12:32:58 1997 +0100
+++ b/src/HOL/List.thy	Thu Mar 06 16:04:23 1997 +0100
@@ -91,8 +91,9 @@
 primrec take list
   take_Nil  "take n [] = []"
   take_Cons "take n (x#xs) = (case n of 0 => [] | Suc(m) => x # take m xs)"
-defs
-  nth_def  "nth(n) == nat_rec hd (%m r xs. r(tl(xs))) n"
+primrec nth nat
+  "nth 0 xs = hd xs"
+  "nth (Suc n) xs = nth n (tl xs)"
 primrec takeWhile list
   "takeWhile P [] = []"
   "takeWhile P (x#xs) = (if P x then x#takeWhile P xs else [])"