1.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Wed May 26 16:31:44 2010 +0200
     1.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Wed May 26 16:44:57 2010 +0200
     1.3 @@ -1101,7 +1101,7 @@
     1.4    THEN (REPEAT_DETERM (CHANGED (asm_simp_tac (simpset_of ctxt) i)));
     1.5  
     1.6  fun pair_tac ctxt s =
     1.7 -  res_inst_tac ctxt [(("p", 0), s)] PairE
     1.8 +  res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
     1.9    THEN' hyp_subst_tac THEN' asm_full_simp_tac (simpset_of ctxt);
    1.10  
    1.11  (* induction on a sequence of pairs with pairsplitting and simplification *)