src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
changeset 59882 ada832308efe
parent 59858 890b68e1e8b6
child 60318 ab785001b51d
     1.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Tue Mar 31 19:16:44 2015 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Tue Mar 31 19:39:05 2015 +0200
     1.3 @@ -737,16 +737,17 @@
     1.4               bnd_def
     1.5  
     1.6      val thm =
     1.7 -      if Name_Space.defined_entry (Theory.axiom_space thy) def_name then
     1.8 -        Thm.axiom thy def_name
     1.9 -      else
    1.10 -        if is_none prob_name_opt then
    1.11 -          (*This mode is for testing, so we can be a bit
    1.12 -            looser with theories*)
    1.13 -          Thm.add_axiom_global (bnd_name, conclusion) thy
    1.14 -          |> fst |> snd
    1.15 -        else
    1.16 -          raise (NO_SKOLEM_DEF (def_name, bnd_name, conclusion))
    1.17 +      (case try (Thm.axiom thy) def_name of
    1.18 +        SOME thm => thm
    1.19 +      | NONE =>
    1.20 +          if is_none prob_name_opt then
    1.21 +            (*This mode is for testing, so we can be a bit
    1.22 +              looser with theories*)
    1.23 +            (* FIXME bad theory context!? *)
    1.24 +            Thm.add_axiom_global (bnd_name, conclusion) thy
    1.25 +            |> fst |> snd
    1.26 +          else
    1.27 +            raise (NO_SKOLEM_DEF (def_name, bnd_name, conclusion)))
    1.28    in
    1.29      rtac (Drule.export_without_context thm) i st
    1.30    end