diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Unix/Unix.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -73,7 +73,7 @@
   \cite{Naraschewski:2001}.}
 *}
 
-datatype perm =
+datatype_new perm =
     Readable
   | Writable
   | Executable    -- "(ignored)"
@@ -284,7 +284,7 @@
   @{text "root \<midarrow>x\<rightarrow> root'"} for the operational semantics.
 *}
 
-datatype operation =
+datatype_new operation =
     Read uid string path
   | Write uid string path
   | Chmod uid perms path