src/HOL/W0/W0.thy

     "free_tv (\<lambda>u::nat. $s1 (s2 u) :: typ) \<subseteq> free_tv s1 \<union> free_tv s2"
   apply (unfold free_tv_subst dom_def)
   apply (tactic {*
     fast_tac (set_cs addSDs [thm "free_tv_app_subst_te" RS subsetD,
     thm "free_tv_subst_var" RS subsetD]
-    addss (simpset() delsimps bex_simps
+    addss (simpset() delsimps (thms "bex_simps")
     addsimps [thm "cod_def", thm "dom_def"])) 1 *})
   done
 
 
 subsection {* Most general unifiers *}

     (v \<in> free_tv s \<or> v \<in> free_tv t) \<Longrightarrow> v < n \<Longrightarrow> v \<in> free_tv a"
   apply (atomize (full))
   apply (induct e)
     txt {* case @{text "Var n"} *}
     apply clarsimp
-    apply (tactic {* fast_tac (HOL_cs addIs [nth_mem, subsetD, thm "ftv_mem_sub_ftv_list"]) 1 *})
+    apply (tactic {* fast_tac (HOL_cs addIs [thm "nth_mem", subsetD, thm "ftv_mem_sub_ftv_list"]) 1 *})
    txt {* case @{text "Abs e"} *}
    apply (simp add: free_tv_subst split add: split_bind)
    apply (intro strip)
    apply (rename_tac s t n1 v)
    apply (erule_tac x = "Suc n" in allE)