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

 fun Seq_Finite_induct_tac ctxt i =
   eresolve_tac ctxt @{thms Seq_Finite_ind} i
   THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt i)));
 
 fun pair_tac ctxt s =
-  Rule_Insts.res_inst_tac ctxt [((("p", 0), Position.none), s)] [] @{thm PairE}
+  Rule_Insts.res_inst_tac ctxt [((("y", 0), Position.none), s)] [] @{thm PairE}
   THEN' hyp_subst_tac ctxt THEN' asm_full_simp_tac ctxt;
 
 (* induction on a sequence of pairs with pairsplitting and simplification *)
 fun pair_induct_tac ctxt s rws i =
   Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] [] @{thm Seq_induct} i