diff -r 639de962ded4 -r 5079fdf938dd src/ZF/Coind/Map.ML
--- a/src/ZF/Coind/Map.ML	Thu Sep 26 15:14:23 1996 +0200
+++ b/src/ZF/Coind/Map.ML	Thu Sep 26 15:49:54 1996 +0200
@@ -175,7 +175,7 @@
 
 goalw Map.thy [map_app_def,map_owr_def] 
   "map_app(map_owr(f,a,b),a) = b";
-by (rtac (qbeta RS ssubst) 1);
+by (stac qbeta 1);
 by (fast_tac ZF_cs 1);
 by (simp_tac if_ss 1);
 qed "map_app_owr1";
@@ -183,7 +183,7 @@
 goalw Map.thy [map_app_def,map_owr_def] 
   "!!a.c ~= a ==> map_app(map_owr(f,a,b),c)= map_app(f,c)";
 by (rtac (excluded_middle RS disjE) 1);
-by (rtac (qbeta_emp RS ssubst) 1);
+by (stac qbeta_emp 1);
 by (assume_tac 1);
 by (fast_tac eq_cs 1);
 by (etac (qbeta RS ssubst) 1);