src/HOL/Unix/Unix.thy

   is member of a single global group.\footnote{A general HOL model of
   user group structures and related issues is given in
   \cite{Naraschewski:2001}.}
 *}
 
-datatype_new perm =
+datatype perm =
     Readable
   | Writable
   | Executable    -- "(ignored)"
 
 type_synonym perms = "perm set"

   operation} for the syntax of system-calls, together with an
   inductive definition of file-system state transitions of the form
   @{text "root \<midarrow>x\<rightarrow> root'"} for the operational semantics.
 *}
 
-datatype_new operation =
+datatype operation =
     Read uid string path
   | Write uid string path
   | Chmod uid perms path
   | Creat uid perms path
   | Unlink uid path