| changeset 27239 | f2f42f9fa09d |
| parent 27208 | 5fe899199f85 |
| child 27809 | a1e409db516b |
--- a/src/HOL/Tools/split_rule.ML Mon Jun 16 17:56:08 2008 +0200 +++ b/src/HOL/Tools/split_rule.ML Mon Jun 16 22:13:39 2008 +0200 @@ -124,7 +124,7 @@ fun pair_tac ctxt s = - RuleInsts.res_inst_tac ctxt [(("p", 0), s)] @{thm PairE} + res_inst_tac ctxt [(("p", 0), s)] @{thm PairE} THEN' hyp_subst_tac THEN' K prune_params_tac;