clarified context;
authorwenzelm
Sun, 29 Mar 2015 17:43:03 +0200
changeset 59836 5e77a35adc67
parent 59835 97872c658a44
child 59837 57820650bd11
clarified context;
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;