src/Pure/Tools/rule_insts.ML

     (binding * string option * mixfix) list -> thm -> thm
   val of_rule: Proof.context -> string option list * string option list ->
     (binding * string option * mixfix) list -> thm -> thm
   val read_instantiate: Proof.context -> (indexname * string) list -> string list -> thm -> thm
   val instantiate_tac: Proof.context -> (indexname * string) list -> string list -> tactic
-  val make_elim_preserve: thm -> thm
+  val make_elim_preserve: Proof.context -> thm -> thm
   val method: (Proof.context -> (indexname * string) list -> thm -> int -> tactic) ->
     (Proof.context -> thm list -> int -> tactic) -> (Proof.context -> Proof.method) context_parser
 end;
 
 structure Rule_Insts: RULE_INSTS =

 val eres_inst_tac = bires_inst_tac true;
 
 
 (* forward resolution *)
 
-fun make_elim_preserve rl =
+fun make_elim_preserve ctxt rl =
   let
     val cert = Thm.cterm_of (Thm.theory_of_thm rl);
     val maxidx = Thm.maxidx_of rl;
     fun cvar xi = cert (Var (xi, propT));
     val revcut_rl' =
       Drule.instantiate_normalize ([], [(cvar ("V", 0), cvar ("V", maxidx + 1)),
         (cvar ("W", 0), cvar ("W", maxidx + 1))]) Drule.revcut_rl;
   in
     (case Seq.list_of
-      (Thm.bicompose {flatten = true, match = false, incremented = false}
+      (Thm.bicompose (SOME ctxt) {flatten = true, match = false, incremented = false}
         (false, rl, Thm.nprems_of rl) 1 revcut_rl')
      of
       [th] => th
     | _ => raise THM ("make_elim_preserve", 1, [rl]))
   end;
 
 (*instantiate and cut -- for atomic fact*)
-fun cut_inst_tac ctxt insts rule = res_inst_tac ctxt insts (make_elim_preserve rule);
+fun cut_inst_tac ctxt insts rule = res_inst_tac ctxt insts (make_elim_preserve ctxt rule);
 
 (*forward tactic applies a rule to an assumption without deleting it*)
 fun forw_inst_tac ctxt insts rule = cut_inst_tac ctxt insts rule THEN' assume_tac;
 
 (*dresolve tactic applies a rule to replace an assumption*)
-fun dres_inst_tac ctxt insts rule = eres_inst_tac ctxt insts (make_elim_preserve rule);
+fun dres_inst_tac ctxt insts rule = eres_inst_tac ctxt insts (make_elim_preserve ctxt rule);
 
 
 (* derived tactics *)
 
 (*deletion of an assumption*)