--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Mar 20 11:53:22 2015 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Mar 20 14:48:04 2015 +0100
@@ -185,7 +185,7 @@
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
@@ -221,7 +221,7 @@
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
@@ -673,7 +673,7 @@
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
@@ -1555,8 +1555,8 @@
["% _ . 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})
@@ -1735,7 +1735,7 @@
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