src/HOL/Option.thy

--- a/src/HOL/Option.thy	Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/Option.thy	Mon Feb 17 13:31:42 2014 +0100
@@ -11,8 +11,7 @@
 datatype_new 'a option =
     =: None
   | Some (the: 'a)
-
-datatype_new_compat option
+datatype_compat option
 
 lemma [case_names None Some, cases type: option]:
   -- {* for backward compatibility -- names of variables differ *}