diff -r 0ff5d55205a4 -r ab920d8112b4 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon May 15 10:34:51 2000 +0200
+++ b/src/HOL/List.thy	Mon May 15 17:30:19 2000 +0200
@@ -83,13 +83,11 @@
 translations  "length"  =>  "size:: _ list => nat"
 
 primrec
-  "hd([]) = arbitrary"
   "hd(x#xs) = x"
 primrec
   "tl([]) = []"
   "tl(x#xs) = xs"
 primrec
-  "last [] = arbitrary"
   "last(x#xs) = (if xs=[] then x else last xs)"
 primrec
   "butlast [] = []"