diff -r 3dfb724db099 -r 601ca8efa000 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/List.thy	Mon Feb 17 13:31:42 2014 +0100
@@ -11,8 +11,7 @@
 datatype_new 'a list (map: map rel: list_all2) =
     =: Nil (defaults tl: "[]")  ("[]")
   | Cons (hd: 'a) (tl: "'a list")  (infixr "#" 65)
-
-datatype_new_compat list
+datatype_compat list
 
 lemma [case_names Nil Cons, cases type: list]:
   -- {* for backward compatibility -- names of variables differ *}