src/HOL/MiniML/MiniML.ML
changeset 13630 a013a9dd370f
parent 9747 043098ba5098
     1.1 --- a/src/HOL/MiniML/MiniML.ML	Mon Oct 07 19:01:51 2002 +0200
     1.2 +++ b/src/HOL/MiniML/MiniML.ML	Tue Oct 08 08:20:17 2002 +0200
     1.3 @@ -90,7 +90,6 @@
     1.4  by (rtac ballI 1);
     1.5  by (etac UN_E 1);
     1.6  by (dtac (dom_S' RS subsetD) 1);
     1.7 -by (rotate_tac 1 1);
     1.8  by (Asm_full_simp_tac 1);
     1.9  by (fast_tac (claset() addDs [free_tv_of_substitutions_extend_to_scheme_lists] 
    1.10                        addIs [free_tv_of_substitutions_extend_to_types RS subsetD]) 1);