--- a/Init_prop.thy	Wed May 22 15:22:50 2013 +0800
+++ b/Init_prop.thy	Thu May 30 09:15:19 2013 +0800
@@ -706,12 +706,14 @@
 
 lemma cpfd2sfds_nil_prop:
   "cpfd2sfds [] p = init_cfds2sfds p"
-apply (simp only:cpfd2sfds_def init_cfds2sfds_def)
+apply (simp only:cpfd2sfds_def init_cfds2sfds_def proc_file_fds_def init_proc_file_fds_def)
 apply (rule set_eqI, rule iffI)
-apply (drule CollectD, rule CollectI, (erule exE)+)
-apply (rule_tac x = fd in exI, rule_tac x = f in exI) defer
-apply (drule CollectD, rule CollectI, (erule exE)+)
-apply (rule_tac x = fd in exI, rule_tac x = f in exI)
+apply (drule CollectD, erule bexE, drule CollectD, erule exE)
+apply (rule CollectI, rule_tac x = fd in bexI) defer
+apply (rule CollectI, rule_tac x = f in exI, simp)
+apply (drule CollectD, erule bexE, drule CollectD, erule exE)
+apply (rule CollectI, rule_tac x = fd in bexI) defer
+apply (rule CollectI, rule_tac x = f in exI)
 using cfd2sfd_nil_prop 
 by auto