src/HOL/HOLCF/IOA/meta_theory/Automata.thy

       (fst(snd(snd(s))),a,fst(snd(snd(t)))):trans_of(C)                       
     else fst(snd(snd(t)))=fst(snd(snd(s)))) &                                 
    (if a:actions(asig_of(D)) then                                             
       (snd(snd(snd(s))),a,snd(snd(snd(t)))):trans_of(D)                       
     else snd(snd(snd(t)))=snd(snd(snd(s)))))"
-  apply (simp (no_asm) add: par_def actions_asig_comp Pair_fst_snd_eq Let_def ioa_projections)
+  apply (simp (no_asm) add: par_def actions_asig_comp prod_eq_iff Let_def ioa_projections)
   done
 
 
 subsection "proof obligation generator for IOA requirements"