1.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Jun 08 16:20:18 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Wed Jun 08 16:20:18 2011 +0200
     1.3 @@ -228,22 +228,23 @@
     1.4    if null atp_proof then Vector.foldl (op @) [] fact_names
     1.5    else fold (add_fact ctxt type_sys facts_offset fact_names) atp_proof []
     1.6  
     1.7 -fun is_conjecture_referred_to_in_proof conjecture_shape =
     1.8 +fun is_conjecture_used_in_proof conjecture_shape =
     1.9    exists (fn Inference (name, _, []) => is_conjecture conjecture_shape name
    1.10             | _ => false)
    1.11  
    1.12 -fun used_facts_in_unsound_atp_proof ctxt type_sys conjecture_shape facts_offset
    1.13 +fun used_facts_in_unsound_atp_proof _ _ _ _ _ [] = NONE
    1.14 +  | used_facts_in_unsound_atp_proof ctxt type_sys conjecture_shape facts_offset
    1.15                                      fact_names atp_proof =
    1.16 -  let
    1.17 -    val used_facts =
    1.18 -      used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof
    1.19 -  in
    1.20 -    if forall (is_locality_global o snd) used_facts andalso
    1.21 -       not (is_conjecture_referred_to_in_proof conjecture_shape atp_proof) then
    1.22 -      SOME (map fst used_facts)
    1.23 -    else
    1.24 -      NONE
    1.25 -  end
    1.26 +    let
    1.27 +      val used_facts =
    1.28 +        used_facts_in_atp_proof ctxt type_sys facts_offset fact_names atp_proof
    1.29 +    in
    1.30 +      if forall (is_locality_global o snd) used_facts andalso
    1.31 +         not (is_conjecture_used_in_proof conjecture_shape atp_proof) then
    1.32 +        SOME (map fst used_facts)
    1.33 +      else
    1.34 +        NONE
    1.35 +    end
    1.36  
    1.37  fun uses_typed_helpers typed_helpers =
    1.38    exists (fn Inference (name, _, []) => is_typed_helper typed_helpers name