# HG changeset patch
# User kuncar
# Date 1332509690 -3600
# Node ID 56adbf5bcc82f2aab466a9d22e3888621b1d8e2b
# Parent  bab1c32c201e109da50a960a45161b76e02ce922
resolve invariant constant name clash

diff -r bab1c32c201e -r 56adbf5bcc82 src/HOL/Unix/Unix.thy
--- a/src/HOL/Unix/Unix.thy	Fri Mar 23 14:29:29 2012 +0100
+++ b/src/HOL/Unix/Unix.thy	Fri Mar 23 14:34:50 2012 +0100
@@ -843,7 +843,9 @@
   neither owned nor writable by @{term user\<^isub>1}.
 *}
 
-definition
+
+
+definition invariant where 
   "invariant root path =
     (\<exists>att dir.
       access root path user\<^isub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and>