1.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Jul 14 15:14:37 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Jul 14 15:14:37 2011 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4      GaveUp |
     1.5      ProofMissing |
     1.6      ProofIncomplete |
     1.7 -    UnsoundProof of bool * string list |
     1.8 +    UnsoundProof of bool option * string list | (* FIXME: doesn't belong here *)
     1.9      CantConnect |
    1.10      TimedOut |
    1.11      Inappropriate |
    1.12 @@ -76,7 +76,7 @@
    1.13    GaveUp |
    1.14    ProofMissing |
    1.15    ProofIncomplete |
    1.16 -  UnsoundProof of bool * string list |
    1.17 +  UnsoundProof of bool option * string list |
    1.18    CantConnect |
    1.19    TimedOut |
    1.20    Inappropriate |
    1.21 @@ -123,11 +123,15 @@
    1.22    | string_for_failure ProofIncomplete =
    1.23      "The prover claims the conjecture is a theorem but provided an incomplete \
    1.24      \proof."
    1.25 -  | string_for_failure (UnsoundProof (false, ss)) =
    1.26 +  | string_for_failure (UnsoundProof (NONE, ss)) =
    1.27 +    "The prover found a type-unsound proof " ^ involving ss ^
    1.28 +    "(or, less likely, your axioms are inconsistent). Specify a sound type \
    1.29 +    \encoding or omit the \"type_enc\" option."
    1.30 +  | string_for_failure (UnsoundProof (SOME false, ss)) =
    1.31      "The prover found a type-unsound proof " ^ involving ss ^
    1.32      "(or, less likely, your axioms are inconsistent). Try passing the \
    1.33 -    \\"full_types\" option to Sledgehammer to avoid such spurious proofs."
    1.34 -  | string_for_failure (UnsoundProof (true, ss)) =
    1.35 +    \\"sound\" option to Sledgehammer to avoid such spurious proofs."
    1.36 +  | string_for_failure (UnsoundProof (SOME true, ss)) =
    1.37      "The prover found a type-unsound proof " ^ involving ss ^
    1.38      "even though a supposedly type-sound encoding was used (or, less likely, \
    1.39      \your axioms are inconsistent). Please report this to the Isabelle \

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 14 15:14:37 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 14 15:14:37 2011 +0200
     2.3 @@ -687,8 +687,11 @@
     2.4                      used_facts_in_unsound_atp_proof ctxt
     2.5                          conjecture_shape facts_offset fact_names atp_proof
     2.6                      |> Option.map (fn facts =>
     2.7 -                           UnsoundProof (is_type_enc_virtually_sound type_enc,
     2.8 -                                         facts |> sort string_ord))
     2.9 +                           UnsoundProof
    2.10 +                               (if is_type_enc_virtually_sound type_enc then
    2.11 +                                  SOME sound
    2.12 +                                else
    2.13 +                                  NONE, facts |> sort string_ord))
    2.14                    | _ => outcome
    2.15                in
    2.16                  ((pool, conjecture_shape, facts_offset, fact_names,