src/HOLCF/IOA/meta_theory/CompoExecs.ML

 \      -->  is_exec_frag A (fst s, Filter_ex2 (asig_of A)$(ProjA2$xs)) &\
 \           is_exec_frag B (snd s, Filter_ex2 (asig_of B)$(ProjB2$xs))";
 
 by (pair_induct_tac "xs" [is_exec_frag_def] 1);
 (* main case *)
-ren "ss a t" 1;
+by (rename_tac "ss a t" 1);
 by (safe_tac set_cs);
 by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2) 1));
 qed"lemma_1_1a";