# HG changeset patch
# User bulwahn
# Date 1315912672 -7200
# Node ID 8df4c332cb1cc16cd17eb38bc1f3e73a5ad644a4
# Parent  840d8c3d91136e625126b23b0380c2072c2b4c35# Parent  635ae0a736886c084aa20dcc9ac3bb7dad9e75f6
merged

diff -r 840d8c3d9113 -r 8df4c332cb1c src/HOL/Tools/ATP/atp_proof.ML
--- 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 \
diff -r 840d8c3d9113 -r 8df4c332cb1c src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- 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)