changeset 13630 | a013a9dd370f |
parent 9747 | 043098ba5098 |
--- a/src/HOL/MiniML/MiniML.ML Mon Oct 07 19:01:51 2002 +0200 +++ b/src/HOL/MiniML/MiniML.ML Tue Oct 08 08:20:17 2002 +0200 @@ -90,7 +90,6 @@ 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);