diff -r 97872c658a44 -r 5e77a35adc67 src/Pure/Tools/rule_insts.ML
--- a/src/Pure/Tools/rule_insts.ML	Sun Mar 29 16:22:35 2015 +0200
+++ b/src/Pure/Tools/rule_insts.ML	Sun Mar 29 17:43:03 2015 +0200
@@ -258,10 +258,8 @@
 
     val thm' = Thm.lift_rule cgoal thm
       |> Drule.instantiate_normalize (inst_tvars', inst_vars')
-      |> singleton (Variable.export inst_ctxt goal_ctxt);
-  in
-    compose_tac goal_ctxt (bires_flag, thm', Thm.nprems_of thm) i
-  end) i st;
+      |> singleton (Variable.export inst_ctxt ctxt);
+  in compose_tac ctxt (bires_flag, thm', Thm.nprems_of thm) i end) i st;
 
 val res_inst_tac = bires_inst_tac false;
 val eres_inst_tac = bires_inst_tac true;