diff -r 548e2d3105b9 -r 5fe899199f85 src/HOL/Tools/split_rule.ML
--- a/src/HOL/Tools/split_rule.ML	Sat Jun 14 17:49:24 2008 +0200
+++ b/src/HOL/Tools/split_rule.ML	Sat Jun 14 23:19:51 2008 +0200
@@ -15,7 +15,7 @@
 sig
   include BASIC_SPLIT_RULE
   val split_rule_var: term -> thm -> thm
-  val split_rule_goal: string list list -> thm -> thm
+  val split_rule_goal: Proof.context -> string list list -> thm -> thm
   val setup: theory -> theory
 end;
 
@@ -123,14 +123,16 @@
   end;
 
 
-fun pair_tac s =
-  EVERY' [res_inst_tac [("p", s)] @{thm PairE}, hyp_subst_tac, K prune_params_tac];
+fun pair_tac ctxt s =
+  RuleInsts.res_inst_tac ctxt [(("p", 0), s)] @{thm PairE}
+  THEN' hyp_subst_tac
+  THEN' K prune_params_tac;
 
 val split_rule_ss = HOL_basic_ss addsimps [split_conv, fst_conv, snd_conv];
 
-fun split_rule_goal xss rl =
+fun split_rule_goal ctxt xss rl =
   let
-    fun one_split i s = Tactic.rule_by_tactic (pair_tac s i);
+    fun one_split i s = Tactic.rule_by_tactic (pair_tac ctxt s i);
     fun one_goal (i, xs) = fold (one_split (i + 1)) xs;
   in
     rl
@@ -148,7 +150,8 @@
   (Scan.lift (Args.parens (Args.$$$ "complete"))
     >> K (Thm.rule_attribute (K complete_split_rule)) ||
   Args.and_list1 (Scan.lift (Scan.repeat Args.name))
-    >> (fn xss => Thm.rule_attribute (K (split_rule_goal xss))));
+    >> (fn xss => Thm.rule_attribute (fn context =>
+        split_rule_goal (Context.proof_of context) xss)));
 
 val setup =
   Attrib.add_attributes