src/HOLCF/FOCUS/Buffer_adm.ML

--- a/src/HOLCF/FOCUS/Buffer_adm.ML	Thu Dec 08 20:15:50 2005 +0100
+++ b/src/HOLCF/FOCUS/Buffer_adm.ML	Thu Dec 08 20:15:57 2005 +0100
@@ -219,7 +219,7 @@
 b y Safe_tac;
 b y rewtac BufAC_Asm_F_def;
 b y Safe_tac;
-b y etac Classical.swap 1;
+b y etac contrapos_np 1;
 b y dtac (fstream_exhaust_eq RS iffD1) 1;
 b y Clarsimp_tac 1;
 b y datac fstream_lub_lemma 1 1;
@@ -230,7 +230,7 @@
 b y Clarify_tac 1;
 b y Simp_tac 1;
 b y rtac disjCI 1;
-b y etac Classical.swap 1;
+b y etac contrapos_np 1;
 b y dtac (fstream_exhaust_eq RS iffD1) 1;
 b y Clarsimp_tac 1;
 b y datac fstream_lub_lemma 1 1;
@@ -252,7 +252,7 @@
 by (rtac BufAC_Asm_def 1);
 b y rewtac BufAC_Asm_F_def;
 b y Safe_tac;
-b y etac Classical.swap 1;
+b y etac contrapos_np 1;
 b y dtac (fstream_exhaust_eq RS iffD1) 1;
 b y Clarsimp_tac 1;
 b y ftac fstream_prefix 1;