1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Sun Feb 05 12:27:10 2012 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Sun Feb 05 12:27:10 2012 +0100
     1.3 @@ -115,7 +115,7 @@
     1.4      "The prover claims the conjecture is a theorem but did not provide a proof."
     1.5    | string_for_failure ProofIncomplete =
     1.6      "The prover claims the conjecture is a theorem but provided an incomplete \
     1.7 -    \proof."
     1.8 +    \(or unparsable) proof."
     1.9    | string_for_failure (UnsoundProof (false, ss)) =
    1.10      "The prover found a type-unsound proof " ^ involving ss ^
    1.11      "(or, less likely, your axioms are inconsistent). Specify a sound type \
    1.12 @@ -431,26 +431,30 @@
    1.13       -- Scan.repeat parse_decorated_atom
    1.14     >> (mk_horn o apfst (op @))) x
    1.15  
    1.16 -fun resolve_spass_num spass_names num =
    1.17 -  case Int.fromString num of
    1.18 -    SOME j => if j > 0 andalso j <= Vector.length spass_names then
    1.19 -                Vector.sub (spass_names, j - 1)
    1.20 -              else
    1.21 -                []
    1.22 -  | NONE => []
    1.23 +fun resolve_spass_num (SOME names) _ _ = names
    1.24 +  | resolve_spass_num NONE spass_names num =
    1.25 +    case Int.fromString num of
    1.26 +      SOME j => if j > 0 andalso j <= Vector.length spass_names then
    1.27 +                  Vector.sub (spass_names, j - 1)
    1.28 +                else
    1.29 +                  []
    1.30 +    | NONE => []
    1.31  
    1.32  val parse_spass_debug =
    1.33    Scan.option ($$ "(" |-- Scan.repeat (scan_general_id --| Scan.option ($$ ","))
    1.34                 --| $$ ")")
    1.35  
    1.36 -(* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms>. *)
    1.37 +(* Syntax: <num>[0:<inference><annotations>] <atoms> || <atoms> -> <atoms>.
    1.38 +           derived from formulae <ident>* *)
    1.39  fun parse_spass_line spass_names =
    1.40    parse_spass_debug |-- scan_general_id --| $$ "[" --| $$ "0" --| $$ ":"
    1.41      -- Symbol.scan_id -- parse_spass_annotations --| $$ "]"
    1.42      -- parse_horn_clause --| $$ "."
    1.43 -  >> (fn (((num, rule), deps), u) =>
    1.44 -         Inference ((num, resolve_spass_num spass_names num), u, rule,
    1.45 -                    map (swap o `(resolve_spass_num spass_names)) deps))
    1.46 +    -- Scan.option (Scan.this_string "derived from formulae "
    1.47 +                    |-- Scan.repeat scan_general_id)
    1.48 +  >> (fn ((((num, rule), deps), u), names) =>
    1.49 +         Inference ((num, resolve_spass_num names spass_names num), u, rule,
    1.50 +                    map (swap o `(resolve_spass_num NONE spass_names)) deps))
    1.51  
    1.52  (* Syntax: <name> *)
    1.53  fun parse_satallax_line x =

     2.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sun Feb 05 12:27:10 2012 +0100
     2.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Sun Feb 05 12:27:10 2012 +0100
     2.3 @@ -211,9 +211,7 @@
     2.4  
     2.5  fun used_facts_in_unsound_atp_proof _ _ [] = NONE
     2.6    | used_facts_in_unsound_atp_proof ctxt fact_names atp_proof =
     2.7 -    let
     2.8 -      val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
     2.9 -    in
    2.10 +    let val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof in
    2.11        if forall (fn (_, (sc, _)) => sc = Global) used_facts andalso
    2.12           not (is_axiom_used_in_proof (is_conjecture o single) atp_proof) then
    2.13          SOME (map fst used_facts)

     3.1 --- a/src/HOL/Tools/ATP/atp_systems.ML	Sun Feb 05 12:27:10 2012 +0100
     3.2 +++ b/src/HOL/Tools/ATP/atp_systems.ML	Sun Feb 05 12:27:10 2012 +0100
     3.3 @@ -360,8 +360,9 @@
     3.4     required_execs =
     3.5       [("SPASS_NEW_HOME", "SPASS"), ("SPASS_NEW_HOME", "tptp2dfg")],
     3.6     arguments = fn _ => fn _ => fn incomplete => fn timeout => fn _ =>
     3.7 -     ("-Auto -LR=1 -LT=1 -Isabelle=1 -TimeLimit=" ^
     3.8 -      string_of_int (to_secs 1 timeout))
     3.9 +     (* TODO: add: -FPDFGProof -FPFCR *)
    3.10 +     ("-Auto -Isabelle=1 -TimeLimit=" ^ string_of_int (to_secs 1 timeout))
    3.11 +     (* TODO: not used yet *)
    3.12       |> incomplete = spass_incompleteN ? prefix "-Splits=0 -FullRed=0 ",
    3.13     proof_delims = #proof_delims spass_config,
    3.14     known_failures = #known_failures spass_config,

     4.1 --- a/src/HOL/Tools/ATP/scripts/spass_new	Sun Feb 05 12:27:10 2012 +0100
     4.2 +++ b/src/HOL/Tools/ATP/scripts/spass_new	Sun Feb 05 12:27:10 2012 +0100
     4.3 @@ -8,7 +8,7 @@
     4.4  name=${@:$(($#)):1}
     4.5  
     4.6  rm -f "$name.prf"
     4.7 -"$SPASS_NEW_HOME/SPASS" -FPDFGProof -FPFCR $options "$name"
     4.8 +"$SPASS_NEW_HOME/SPASS" $options "$name"
     4.9  if [ -f "$name.prf" ]
    4.10  then
    4.11    cat "$name.prf"

     5.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Feb 05 12:27:10 2012 +0100
     5.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Sun Feb 05 12:27:10 2012 +0100
     5.3 @@ -746,8 +746,11 @@
     5.4                         SOME facts =>
     5.5                         let
     5.6                           val failure =
     5.7 -                           UnsoundProof (is_type_enc_quasi_sound type_enc,
     5.8 -                                         facts)
     5.9 +                           if null facts then
    5.10 +                             ProofIncomplete
    5.11 +                           else
    5.12 +                             UnsoundProof (is_type_enc_quasi_sound type_enc,
    5.13 +                                           facts)
    5.14                         in
    5.15                           if debug then
    5.16                             (warning (string_for_failure failure); NONE)