# HG changeset patch
# User paulson
# Date 875526745 -7200
# Node ID bed0ba7bff2f8bd972b128cbd05610220f393d86
# Parent  33f355f56f8204cc53d1df1f77fe0da5889722a8
Step_tac -> Safe_tac

diff -r 33f355f56f82 -r bed0ba7bff2f 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);