# HG changeset patch
# User blanchet
# Date 1307542818 -7200
# Node ID 9f33b4ec866ce34136fc709add059b75b1f40a0e
# Parent  07eb0ad9bb93550e51ea0c0b6e98b437f439d4bd
don't generate unsound proof error for missing proofs

diff -r 07eb0ad9bb93 -r 9f33b4ec866c src/HOL/Tools/ATP/atp_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Jun 08 16:20:18 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Jun 08 16:20:18 2011 +0200
@@ -228,22 +228,23 @@
   if null atp_proof then Vector.foldl (op @) [] fact_names
   else fold (add_fact ctxt type_sys facts_offset fact_names) atp_proof []
 
-fun is_conjecture_referred_to_in_proof conjecture_shape =
+fun is_conjecture_used_in_proof conjecture_shape =
   exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name
            | _ => false)
 
-fun used_facts_in_unsound_atp_proof ctxt type_sys conjecture_shape facts_offset
+fun used_facts_in_unsound_atp_proof _ _ _ _ _ [] = NONE
+  | used_facts_in_unsound_atp_proof ctxt type_sys conjecture_shape facts_offset
                                     fact_names atp_proof =
-  let
-    val used_facts =
-      used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof
-  in
-    if forall (is_locality_global o snd) used_facts andalso
-       not (is_conjecture_referred_to_in_proof conjecture_shape atp_proof) then
-      SOME (map fst used_facts)
-    else
-      NONE
-  end
+    let
+      val used_facts =
+        used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof
+    in
+      if forall (is_locality_global o snd) used_facts andalso
+         not (is_conjecture_used_in_proof conjecture_shape atp_proof) then
+        SOME (map fst used_facts)
+      else
+        NONE
+    end
 
 fun uses_typed_helpers typed_helpers =
   exists (fn Inference (name, _, []) => is_typed_helper typed_helpers name