src/HOL/TPTP/TPTP_Proof_Reconstruction.thy

   in
     if null parameters then no_tac st
     else
       let
         fun instantiate param =
-           (map (eres_inst_tac ctxt [((("x", 0), Position.none), param)]) thms
+          (map (Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), param)]) thms
                    |> FIRST')
         val attempts = map instantiate parameters
       in
         (fold (curry (op APPEND')) attempts (K no_tac)) i st
       end

   in
     if null parameters then no_tac st
     else
       let
         fun instantiates param =
-           eres_inst_tac ctxt [((("x", 0), Position.none), param)] thm
+          Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), param)] thm
 
         val quantified_var = head_quantified_variable ctxt i st
       in
         if is_none quantified_var then no_tac st
         else

   in
     if null gls orelse null candidate_consts then no_tac st
     else
       let
         fun instantiate const_name =
-          dres_inst_tac ctxt [((("sk", 0), Position.none), const_name ^ parameters)]
+          Rule_Insts.dres_inst_tac ctxt [((("sk", 0), Position.none), const_name ^ parameters)]
             @{thm leo2_skolemise}
         val attempts = map instantiate candidate_consts
       in
         (fold (curry (op APPEND')) attempts (K no_tac)) i st
       end

 
     val bool_to_bool =
       ["% _ . True", "% _ . False", "% x . x", "Not"]
 
     val tecs =
-      map (fn t_s =>
-       eres_inst_tac @{context} [((("x", 0), Position.none), t_s)] @{thm allE}
+      map (fn t_s =>  (* FIXME proper context!? *)
+       Rule_Insts.eres_inst_tac @{context} [((("x", 0), Position.none), t_s)] @{thm allE}
        THEN' atac)
   in
     (TRY o etac @{thm forall_pos_lift})
     THEN' (atac
            ORELSE' FIRST'

             if null hyp_prefix orelse
               member (op =) conc_prefix (hd hyp_prefix) orelse
               member (op =)  (Term.add_frees hyp_body []) (hd hyp_prefix) then
               no_tac st
             else
-              eres_inst_tac ctxt [((("x", 0), Position.none), "(@X. False)")]
+              Rule_Insts.eres_inst_tac ctxt [((("x", 0), Position.none), "(@X. False)")]
                 @{thm allE} i st
           end
      end
   end
 *}