--- a/src/HOL/Tools/ATP/atp_proof.ML Tue Sep 13 12:14:29 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML Tue Sep 13 13:17:52 2011 +0200
@@ -19,7 +19,7 @@
GaveUp |
ProofMissing |
ProofIncomplete |
- UnsoundProof of bool option * string list | (* FIXME: doesn't belong here *)
+ UnsoundProof of bool * string list |
CantConnect |
TimedOut |
Inappropriate |
@@ -76,7 +76,7 @@
GaveUp |
ProofMissing |
ProofIncomplete |
- UnsoundProof of bool option * string list |
+ UnsoundProof of bool * string list |
CantConnect |
TimedOut |
Inappropriate |
@@ -120,15 +120,11 @@
| string_for_failure ProofIncomplete =
"The prover claims the conjecture is a theorem but provided an incomplete \
\proof."
- | string_for_failure (UnsoundProof (NONE, ss)) =
+ | string_for_failure (UnsoundProof (false, ss)) =
"The prover found a type-unsound proof " ^ involving ss ^
"(or, less likely, your axioms are inconsistent). Specify a sound type \
\encoding or omit the \"type_enc\" option."
- | string_for_failure (UnsoundProof (SOME false, ss)) =
- "The prover found a type-unsound proof " ^ involving ss ^
- "(or, less likely, your axioms are inconsistent). Try passing the \
- \\"sound\" option to Sledgehammer to avoid such spurious proofs."
- | string_for_failure (UnsoundProof (SOME true, ss)) =
+ | string_for_failure (UnsoundProof (true, ss)) =
"The prover found a type-unsound proof " ^ involving ss ^
"even though a supposedly type-sound encoding was used (or, less likely, \
\your axioms are inconsistent). Please report this to the Isabelle \
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Sep 13 12:14:29 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Sep 13 13:17:52 2011 +0200
@@ -696,9 +696,8 @@
SOME facts =>
let
val failure =
- (if is_type_enc_quasi_sound type_enc then SOME sound
- else NONE, facts)
- |> UnsoundProof
+ UnsoundProof (is_type_enc_quasi_sound type_enc,
+ facts)
in
if debug then
(warning (string_for_failure failure); NONE)