--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Tue Mar 31 19:16:44 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Tue Mar 31 19:39:05 2015 +0200
@@ -737,16 +737,17 @@
bnd_def
val thm =
- if Name_Space.defined_entry (Theory.axiom_space thy) def_name then
- Thm.axiom thy def_name
- else
- if is_none prob_name_opt then
- (*This mode is for testing, so we can be a bit
- looser with theories*)
- Thm.add_axiom_global (bnd_name, conclusion) thy
- |> fst |> snd
- else
- raise (NO_SKOLEM_DEF (def_name, bnd_name, conclusion))
+ (case try (Thm.axiom thy) def_name of
+ SOME thm => thm
+ | NONE =>
+ if is_none prob_name_opt then
+ (*This mode is for testing, so we can be a bit
+ looser with theories*)
+ (* FIXME bad theory context!? *)
+ Thm.add_axiom_global (bnd_name, conclusion) thy
+ |> fst |> snd
+ else
+ raise (NO_SKOLEM_DEF (def_name, bnd_name, conclusion)))
in
rtac (Drule.export_without_context thm) i st
end