diff -r 21238c9d363e -r a129b817b58a src/CCL/CCL.ML
--- a/src/CCL/CCL.ML	Tue Dec 16 15:17:26 1997 +0100
+++ b/src/CCL/CCL.ML	Tue Dec 16 17:58:03 1997 +0100
@@ -166,8 +166,8 @@
 \                (EX a a' b b'. t=<a,b> &  t'=<a',b'>  & a [= a' & b [= b') | \
 \                (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. f(x) [= f'(x)))";
 by (simp_tac (ccl_ss addsimps [PO_iff] delsimps ex_simps) 1);
-br (rewrite_rule [POgen_def,SIM_def] 
-                 (POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1;
+by (rtac (rewrite_rule [POgen_def,SIM_def] 
+                 (POgen_mono RS (PO_def RS def_gfp_Tarski) RS XHlemma1)) 1);
 by (rtac (iff_refl RS XHlemma2) 1);
 qed "poXH";
 
@@ -292,8 +292,8 @@
 \             (EX f f'. t=lam x. f(x) &  t'=lam x. f'(x) & (ALL x. <f(x),f'(x)> : EQ))" 1);
 by (etac rev_mp 1);
 by (simp_tac (CCL_ss addsimps [EQ_iff RS iff_sym]) 1);
-br (rewrite_rule [EQgen_def,SIM_def]
-                 (EQgen_mono RS (EQ_def RS def_gfp_Tarski) RS XHlemma1)) 1;
+by (rtac (rewrite_rule [EQgen_def,SIM_def]
+                 (EQgen_mono RS (EQ_def RS def_gfp_Tarski) RS XHlemma1)) 1);
 by (rtac (iff_refl RS XHlemma2) 1);
 qed "eqXH";