changeset 36546 | a9873318fe30 |
parent 35365 | 2fcd08c62495 |
child 36960 | 01594f816e3a |
--- a/src/HOL/Tools/split_rule.ML Fri Apr 30 17:18:29 2010 +0200 +++ b/src/HOL/Tools/split_rule.ML Fri Apr 30 18:06:29 2010 +0200 @@ -116,7 +116,7 @@ fun split_rule_goal ctxt xss rl = let - fun one_split i s = Tactic.rule_by_tactic (pair_tac ctxt s i); + fun one_split i s = Tactic.rule_by_tactic ctxt (pair_tac ctxt s i); fun one_goal (i, xs) = fold (one_split (i + 1)) xs; in rl