--- a/Dynamic2static.thy	Thu Jun 06 12:38:44 2013 +0800
+++ b/Dynamic2static.thy	Thu Jun 06 14:50:52 2013 +0800
@@ -213,12 +213,8 @@
 apply (case_tac obj, simp_all split:option.splits if_splits)
 apply (drule_tac sm = "(aa, ba, True)" in sq_sm_prop, simp+, erule exE)
 apply (rule_tac x = "O_msg nat m" in exI)
-apply (simp)
-
-apply (case_tac obj, (simp split:option.splits if_splits)+)
-apply (erule conjE, drule_tac )
-
-
+apply (simp add:cm2smsg_def split:option.splits)
+done
 
 lemma has_inode_tainted_aux:
   "O_file f \<in> tainted s \<Longrightarrow> \<forall> f'. has_same_inode s f f' \<longrightarrow> O_file f' \<in> tainted s"