--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Thu Mar 19 17:25:57 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy Thu Mar 19 22:30:57 2015 +0100
@@ -1081,7 +1081,7 @@
ML {*
fun Seq_case_tac ctxt s i =
- res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_cases} i
+ res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_cases} i
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 *)
@@ -1093,7 +1093,7 @@
(* rws are definitions to be unfolded for admissibility check *)
fun Seq_induct_tac ctxt s rws i =
- res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
+ res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_induct} i
THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt (i+1))))
THEN simp_tac (ctxt addsimps rws) i;
@@ -1102,12 +1102,12 @@
THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ctxt i)));
fun pair_tac ctxt s =
- res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
+ res_inst_tac ctxt [((("p", 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 =
- res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
+ res_inst_tac ctxt [((("x", 0), Position.none), s)] @{thm Seq_induct} i
THEN pair_tac ctxt "a" (i+3)
THEN (REPEAT_DETERM (CHANGED (simp_tac ctxt (i+1))))
THEN simp_tac (ctxt addsimps rws) i;