Step_tac -> Safe_tac
authorpaulson
Mon, 29 Sep 1997 11:52:25 +0200
changeset 3735 bed0ba7bff2f
parent 3734 33f355f56f82
child 3736 39ee3d31cfbc
Step_tac -> Safe_tac
src/ZF/Coind/Map.ML
--- 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);