src/HOL/MiniML/MiniML.ML
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);