# HG changeset patch
# User wenzelm
# Date 1427823545 -7200
# Node ID ada832308efe39699fff7695ebea920cd691a4ec
# Parent  547bf78e5d4d66d738885a909adee244cdab56fd
tuned -- avoid exotic Name_Space.defined_entry;

diff -r 547bf78e5d4d -r ada832308efe src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- 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