# HG changeset patch
# User blanchet
# Date 1384886550 -3600
# Node ID 8b5caa190054c1d21191c66f3cd078dddb5c0613
# Parent  d023838eb2529463bbc4f2bdf5818c263a0de8b7
tuning

diff -r d023838eb252 -r 8b5caa190054 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Nov 19 19:36:24 2013 +0100
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Nov 19 19:42:30 2013 +0100
@@ -368,8 +368,8 @@
       s' |> find_first_in_list_vector fact_names |> Option.map (pair s')
     end
   | NONE => NONE
+
 fun resolve_fact fact_names = map_filter (resolve_one_named_fact fact_names)
-fun is_fact fact_names = not o null o resolve_fact fact_names
 
 fun resolve_one_named_conjecture s =
   case try (unprefix conjecture_prefix) s of
@@ -377,7 +377,6 @@
   | NONE => NONE
 
 val resolve_conjecture = map_filter resolve_one_named_conjecture
-val is_conjecture = not o null o resolve_conjecture
 
 fun is_axiom_used_in_proof pred =
   exists (fn ((_, ss), _, _, _, []) => exists pred ss | _ => false)
@@ -428,7 +427,7 @@
   | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof =
     let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof in
       if forall (fn (_, (sc, _)) => sc = Global) used_facts andalso
-         not (is_axiom_used_in_proof (is_conjecture o single) atp_proof) then
+         not (is_axiom_used_in_proof (not o null o resolve_conjecture o single) atp_proof) then
         SOME (map fst used_facts)
       else
         NONE