1.1 --- a/src/HOL/Unix/Unix.thy	Sat Jan 15 17:32:07 2011 +0100
     1.2 +++ b/src/HOL/Unix/Unix.thy	Sat Jan 15 18:12:26 2011 +0100
     1.3 @@ -47,10 +47,9 @@
     1.4    names and user ids as would be present in a reality.
     1.5  *}
     1.6  
     1.7 -types
     1.8 -  uid = nat
     1.9 -  name = nat
    1.10 -  path = "name list"
    1.11 +type_synonym uid = nat
    1.12 +type_synonym name = nat
    1.13 +type_synonym path = "name list"
    1.14  
    1.15  
    1.16  subsection {* Attributes *}
    1.17 @@ -80,7 +79,7 @@
    1.18    | Writable
    1.19    | Executable    -- "(ignored)"
    1.20  
    1.21 -types perms = "perm set"
    1.22 +type_synonym perms = "perm set"
    1.23  
    1.24  record att =
    1.25    owner :: uid
    1.26 @@ -132,8 +131,7 @@
    1.27    of directory nodes).
    1.28  *}
    1.29  
    1.30 -types
    1.31 -  "file" = "(att \<times> string, att, name) env"
    1.32 +type_synonym "file" = "(att \<times> string, att, name) env"
    1.33  
    1.34  text {*
    1.35    \medskip The HOL library also provides @{term lookup} and @{term