--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sun Jun 22 06:16:56 2014 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sun Jun 22 06:16:57 2014 +0100
@@ -2116,7 +2116,10 @@
in
case inference_name of
"fo_atp_e" =>
+ HEADGOAL (Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt [])
+ (*NOTE To treat E as an oracle use the following line:
HEADGOAL (etac (oracle_based_reconstruction_tac ctxt prob_name node))
+ *)
| "copy" =>
HEADGOAL
(atac
@@ -2284,4 +2287,4 @@
end
*}
-end
\ No newline at end of file
+end