src/HOLCF/IOA/meta_theory/CompoTraces.ML

 "!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A; \
 \           is_asig(asig_of A); is_asig(asig_of B)|] \
 \==> Traces (A||B) = par_traces (Traces A) (Traces B)";
 
 by (asm_full_simp_tac (simpset() addsimps [asig_of_par]) 1);
-br set_ext 1;
+by (rtac set_ext 1);
 by (asm_full_simp_tac (simpset() addsimps [compositionality_tr,externals_of_par]) 1);
 qed"compositionality_tr_modules";