--- a/os_rc.thy	Sat Dec 14 13:07:41 2013 +1100
+++ b/os_rc.thy	Thu Dec 25 15:54:08 2014 +0000
@@ -352,7 +352,7 @@
 apply (simp add:fname_length_set_def) 
 apply (rule finite_imageI) using finite_cf[where s = s]
 apply (drule_tac h = "\<lambda> f'. case f' of [] \<Rightarrow> '''' | fn # pf' \<Rightarrow> if (pf' = f) then fn else ''''" in finite_imageI)
-apply (rule_tac B = "(list_case [] (\<lambda>fn pf'. if pf' = f then fn else []) ` current_files s)" in finite_subset)
+apply (rule_tac B = "(case_list [] (\<lambda>fn pf'. if pf' = f then fn else []) ` current_files s)" in finite_subset)
 unfolding image_def
 apply(auto)[1]
 apply (rule_tac x = "x # f" in bexI, simp+)