# HG changeset patch
# User wenzelm
# Date 1129911420 -7200
# Node ID d20a9dd2a68c73b5d93ef316350aa13f57cd5127
# Parent  2602be0d99aeadde1a3d4d3ebed13fc2099ad314
avoid OldGoals shortcuts;

diff -r 2602be0d99ae -r d20a9dd2a68c src/HOLCF/IOA/Storage/Correctness.ML
--- a/src/HOLCF/IOA/Storage/Correctness.ML	Fri Oct 21 18:16:57 2005 +0200
+++ b/src/HOLCF/IOA/Storage/Correctness.ML	Fri Oct 21 18:17:00 2005 +0200
@@ -26,7 +26,7 @@
 
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
-ren "k b used c k' b' a" 1;
+by (rename_tac "k b used c k' b' a" 1);
 by (induct_tac "a" 1);
 by (ALLGOALS (simp_tac (simpset() addsimps [sim_relation_def,
       thm"Impl.ioa_def",thm "Impl.trans_def",trans_of_def])));