src/ZF/Coind/Map.ML
changeset 3735 bed0ba7bff2f
parent 2493 bdeb5024353a
child 3840 e0baea4d485a
--- a/src/ZF/Coind/Map.ML	Mon Sep 29 11:51:52 1997 +0200
+++ b/src/ZF/Coind/Map.ML	Mon Sep 29 11:52:25 1997 +0200
@@ -78,7 +78,7 @@
 
 goalw Map.thy [map_owr_def,PMap_def,TMap_def] 
   "!! A.[| m:PMap(A,B); a:A; b:B |]  ==> map_owr(m,a,b):PMap(A,B)";
-by (Step_tac 1);
+by Safe_tac;
 by (ALLGOALS (asm_full_simp_tac (!simpset addsimps [if_iff])));
 by (Fast_tac 1);
 by (Fast_tac 1);