diff -r ee0838d89deb -r af8008e4de96 src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Tue Jan 30 18:57:24 2001 +0100
+++ b/src/HOL/Unix/Unix.thy	Tue Jan 30 23:53:46 2001 +0100
@@ -975,7 +975,7 @@
   performed by @{term user1} alone.  Note that this holds for any
   @{term path} given, the particular @{term bogus_path} is not
   required here.
-*}  (* FIXME The overall structure of the proof is as follows \dots *)
+*}
 
 lemma preserve_invariant: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow>
   invariant root path \<Longrightarrow> uid_of x = user1 \<Longrightarrow> invariant root' path"