src/HOL/List.thy

--- a/src/HOL/List.thy	Fri May 23 14:52:45 1997 +0200
+++ b/src/HOL/List.thy	Fri May 23 18:17:53 1997 +0200
@@ -49,10 +49,10 @@
   pred_list_def "pred_list == {(x,y). ? h. y = h#x}"
 
 primrec hd list
-  "hd([]) = (@x.False)"
+  "hd([]) = arbitrary"
   "hd(x#xs) = x"
 primrec tl list
-  "tl([]) = (@x.False)"
+  "tl([]) = arbitrary"
   "tl(x#xs) = xs"
 primrec ttl list
   (* a "total" version of tl: *)