clearer unsound message

--- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Jul 14 15:14:37 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Jul 14 15:14:37 2011 +0200
@@ -19,7 +19,7 @@
     GaveUp |
     ProofMissing |
     ProofIncomplete |
-    UnsoundProof of bool * string list |
+    UnsoundProof of bool option * string list | (* FIXME: doesn't belong here *)
     CantConnect |
     TimedOut |
     Inappropriate |
@@ -76,7 +76,7 @@
   GaveUp |
   ProofMissing |
   ProofIncomplete |
-  UnsoundProof of bool * string list |
+  UnsoundProof of bool option * string list |
   CantConnect |
   TimedOut |
   Inappropriate |
@@ -123,11 +123,15 @@
   | string_for_failure ProofIncomplete =
     "The prover claims the conjecture is a theorem but provided an incomplete \
     \proof."
-  | string_for_failure (UnsoundProof (false, ss)) =
+  | string_for_failure (UnsoundProof (NONE, 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 \
-    \\"full_types\" option to Sledgehammer to avoid such spurious proofs."
-  | string_for_failure (UnsoundProof (true, ss)) =
+    \\"sound\" option to Sledgehammer to avoid such spurious proofs."
+  | string_for_failure (UnsoundProof (SOME 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	Thu Jul 14 15:14:37 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jul 14 15:14:37 2011 +0200
@@ -687,8 +687,11 @@
                     used_facts_in_unsound_atp_proof ctxt
                         conjecture_shape facts_offset fact_names atp_proof
                     |> Option.map (fn facts =>
-                           UnsoundProof (is_type_enc_virtually_sound type_enc,
-                                         facts |> sort string_ord))
+                           UnsoundProof
+                               (if is_type_enc_virtually_sound type_enc then
+                                  SOME sound
+                                else
+                                  NONE, facts |> sort string_ord))
                   | _ => outcome
               in
                 ((pool, conjecture_shape, facts_offset, fact_names,