diff -r dfde07c7cd6b -r 042e1e7fd505 no_shm_selinux/Enrich.thy
--- a/no_shm_selinux/Enrich.thy	Thu Jan 09 19:09:09 2014 +0800
+++ b/no_shm_selinux/Enrich.thy	Thu Jan 09 22:53:45 2014 +0800
@@ -7,6 +7,7 @@
 datatype t_enrich_obj = 
   E_proc "t_process" "t_msgq" "t_msgq"
 | E_file "t_file" "nat" 
+| E_file_link "t_file"
 | E_msgq "t_msgq"
 
 (* objects that need dynamic indexing, all nature-numbers *)