--- a/src/HOLCF/FOCUS/Buffer_adm.ML Wed Dec 07 15:23:22 2005 +0100
+++ b/src/HOLCF/FOCUS/Buffer_adm.ML Wed Dec 07 16:47:04 2005 +0100
@@ -219,7 +219,7 @@
b y Safe_tac;
b y rewtac BufAC_Asm_F_def;
b y Safe_tac;
-b y etac swap 1;
+b y etac Classical.swap 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 swap 1;
+b y etac Classical.swap 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 swap 1;
+b y etac Classical.swap 1;
b y dtac (fstream_exhaust_eq RS iffD1) 1;
b y Clarsimp_tac 1;
b y ftac fstream_prefix 1;