src/HOL/List.thy

--- a/src/HOL/List.thy	Tue Jun 10 11:38:53 2014 +0200
+++ b/src/HOL/List.thy	Tue Jun 10 12:16:22 2014 +0200
@@ -9,8 +9,10 @@
 begin
 
 datatype_new (set: 'a) list  (map: map rel: list_all2) =
-    Nil (defaults tl: "[]")  ("[]")
+    Nil  ("[]")
   | Cons (hd: 'a) (tl: "'a list")  (infixr "#" 65)
+where
+  "tl [] = []"
 
 datatype_compat list