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

 
 ML {*
 
 fun Seq_case_tac ctxt s i =
   res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_cases} i
-  THEN hyp_subst_tac i THEN hyp_subst_tac (i+1) THEN hyp_subst_tac (i+2);
+  THEN hyp_subst_tac ctxt i THEN hyp_subst_tac ctxt (i+1) THEN hyp_subst_tac ctxt (i+2);
 
 (* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
 fun Seq_case_simp_tac ctxt s i =
   Seq_case_tac ctxt s i
   THEN asm_simp_tac ctxt (i+2)

   etac @{thm Seq_Finite_ind} i
   THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt i)));
 
 fun pair_tac ctxt s =
   res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
-  THEN' hyp_subst_tac THEN' asm_full_simp_tac ctxt;
+  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 =
   res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
   THEN pair_tac ctxt "a" (i+3)