1.1 --- a/src/HOL/Unix/Unix.thy	Fri Mar 30 13:12:02 2012 +0200
     1.2 +++ b/src/HOL/Unix/Unix.thy	Fri Mar 30 15:25:47 2012 +0200
     1.3 @@ -845,7 +845,7 @@
     1.4  
     1.5  
     1.6  
     1.7 -definition invariant where 
     1.8 +definition
     1.9    "invariant root path =
    1.10      (\<exists>att dir.
    1.11        access root path user\<^isub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and>