--- a/Init_prop.thy	Tue Sep 03 07:25:39 2013 +0800
+++ b/Init_prop.thy	Tue Sep 03 09:31:40 2013 +0800
@@ -769,7 +769,6 @@
             dest:init_same_inode_prop1 
                split:option.splits)
 apply (rule_tac x = list in exI, simp add:init_same_inode_files_def)
-apply (drule is_init_file_prop1, simp add:init_files_props)
 done
 
 lemma s2ss_nil_prop: