src/HOL/MiniML/MiniML.ML

 \  cod (%n. if n : free_tv A Un free_tv t then S n else TVar n) <= \
 \  free_tv ($ S A) Un free_tv ($ S t)";
 by (rtac ballI 1);
 by (etac UN_E 1);
 by (dtac (dom_S' RS subsetD) 1);
-by (rotate_tac 1 1);
 by (Asm_full_simp_tac 1);
 by (fast_tac (claset() addDs [free_tv_of_substitutions_extend_to_scheme_lists] 
                       addIs [free_tv_of_substitutions_extend_to_types RS subsetD]) 1);
 qed "cod_S'";