src/HOLCF/FOCUS/Buffer_adm.ML

 by (rtac def_gfp_admI 1);
 by (rtac BufAC_Asm_def 1);
 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;
 b y Clarify_tac 1;
 b y eres_inst_tac [("x","j")] all_dupE 1;
 b y Asm_full_simp_tac 1;
 b y dtac (BufAC_Asm_d2) 1;
 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;
 b y Clarsimp_tac 1;
 b y simp_tac (HOL_basic_ss addsimps (ex_simps@all_simps RL[sym])) 1;

 Goal "adm (\\<lambda>u. u \\<notin> BufAC_Asm)"; (* uses antitonP *)
 by (rtac def_gfp_adm_nonP 1);
 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;
 b y Clarsimp_tac 1;
 b y ftac BufAC_Asm_d2 1;