src/ZF/Coind/MT.ML

 \     v_clos(x,e,ve_owr(ve,f,cl)) = cl;                         \ 
 \     hastyenv(ve,te); <te,e_fix(f,x,e),t>:ElabRel |] ==>       \
 \  <cl,t>:HasTyRel";
 by (cut_facts_tac prems 1);
 by (etac elab_fixE 1);
-by (safe_tac (claset()));
+by Safe_tac;
 by (EVERY [forward_tac [subst] 1,atac 2,rtac htr_closCI 1]);
 by clean_tac;
 by (rtac ve_owrI 1);
 by clean_tac;
 by (dtac (ElabRel.dom_subset RS subsetD) 1);

 by (assume_tac 1);
 by (assume_tac 1);
 by (etac htr_closE 1);
 by (etac elab_fnE 1);
 by (rewrite_tac Ty.con_defs);
-by (safe_tac (claset()));
+by Safe_tac;
 by (dtac (spec RS spec RS mp RS mp) 1);
 by (assume_tac 3);
 by (assume_tac 2);
 by (rtac hastyenv_owr 1);
 by (assume_tac 1);