diff -r 0a68c605ae79 -r e79e3a8a4ceb no_shm_selinux/Flask.thy
--- a/no_shm_selinux/Flask.thy	Mon Dec 23 19:47:17 2013 +0800
+++ b/no_shm_selinux/Flask.thy	Thu Dec 26 10:56:50 2013 +0800
@@ -510,7 +510,7 @@
   "info_flow_shm s from to \<equiv> (self_shm s from to) \<or> (\<exists> h. one_flow_shm s h from to)" 
 *)
 
-fun current_msgqs :: "t_state \<Rightarrow> t_msg set"
+fun current_msgqs :: "t_state \<Rightarrow> t_msgq set"
 where
   "current_msgqs [] = init_msgqs"
 | "current_msgqs (CreateMsgq p q # \<tau>) = insert q (current_msgqs \<tau>)"