diff -r 0a01efff43e9 -r 7ad150f5fc10 src/HOLCF/FOCUS/Buffer_adm.ML
--- a/src/HOLCF/FOCUS/Buffer_adm.ML	Wed Dec 12 19:22:21 2001 +0100
+++ b/src/HOLCF/FOCUS/Buffer_adm.ML	Wed Dec 12 20:37:31 2001 +0100
@@ -86,7 +86,7 @@
  (K [
 	rtac (BufAC_Cmt_unfold RS iffD2) 1,
 	strip_tac 1,
-	forward_tac [Buf_f_d_req] 1,
+	ftac Buf_f_d_req 1,
 	auto_tac (claset() addEs [BufAC_Asm_cong RS subst],simpset())]);
 
 (*adm_BufAC_Asm*)
@@ -118,7 +118,7 @@
 by (strip_tac 1);
 by (stac BufAC_Cmt_F_def3 1);
 by (dres_inst_tac [("P","%x. x")] (BufAC_Cmt_F_def3 RS subst) 1);
-by (Safe_tac);
+by Safe_tac;
 by (   etac Buf_f_empty 1);
 by (  etac Buf_f_d 1);
 by ( dtac Buf_f_d_req 1);
@@ -215,8 +215,8 @@
 (**** new approach for admissibility, reduces itself to absurdity *************)
 
 Goal "adm (\\<lambda>x. x\\<in>BufAC_Asm)";
-by(rtac def_gfp_admI 1);
-by(rtac BufAC_Asm_def 1);
+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;
@@ -238,7 +238,7 @@
 b y Clarsimp_tac 1;
 b y simp_tac (HOL_basic_ss addsimps (ex_simps@all_simps RL[sym])) 1;
 b y res_inst_tac [("x","Xa")] exI 1;
-br allI 1;
+by (rtac allI 1);
 b y rotate_tac ~1 1;
 b y eres_inst_tac [("x","i")] allE 1;
 b y Clarsimp_tac 1;
@@ -271,8 +271,8 @@
 qed "adm_non_BufAC_Asm";
 
 Goal "f \\<in> BufEq \\<Longrightarrow> adm (\\<lambda>u. u \\<in> BufAC_Asm \\<longrightarrow> (u, f\\<cdot>u) \\<in> BufAC_Cmt)";
-by(rtac triv_admI 1);
-by(Clarify_tac 1);
-by(eatac Buf_Eq_imp_AC_lemma 1 1); 
+by (rtac triv_admI 1);
+by (Clarify_tac 1);
+by (eatac Buf_Eq_imp_AC_lemma 1 1); 
       (* this is what we originally aimed to show, using admissibilty :-( *)
 qed "adm_BufAC";