automatically retry with full-types upon unsound proof

--- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Apr 21 22:18:28 2011 +0200
+++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Apr 21 22:32:00 2011 +0200
@@ -96,7 +96,7 @@
   | string_for_failure ProofMissing =
     "The prover claims the conjecture is a theorem but did not provide a proof."
   | string_for_failure UnsoundProof =
-    "The prover found a type-incorrect proof. (Or, very unlikely, your axioms \
+    "The prover found a type-unsound proof. (Or, very unlikely, your axioms \
     \are inconsistent.)"
   | string_for_failure CantConnect = "Cannot connect to remote server."
   | string_for_failure TimedOut = "Timed out."

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Apr 21 22:18:28 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Apr 21 22:32:00 2011 +0200
@@ -401,7 +401,8 @@
                 |> filter_out (curry (op =) ~1 o fst)
                 |> map (Untranslated_Fact o apfst (fst o nth facts))
               end
-            fun run_slice (slice, (time_frac, (complete, default_max_relevant)))
+            fun run_slice type_sys
+                          (slice, (time_frac, (complete, default_max_relevant)))
                           time_left =
               let
                 val num_facts =
@@ -479,16 +480,22 @@
                  (output, msecs, atp_proof, outcome))
               end
             val timer = Timer.startRealTimer ()
-            fun maybe_run_slice slice (_, (_, msecs0, _, SOME _)) =
-                run_slice slice (Time.- (timeout, Timer.checkRealTimer timer))
+            fun maybe_run_slice type_sys slice (_, (_, msecs0, _, SOME _)) =
+                run_slice type_sys slice
+                          (Time.- (timeout, Timer.checkRealTimer timer))
                 |> (fn (stuff, (output, msecs, atp_proof, outcome)) =>
                        (stuff, (output, int_opt_add msecs0 msecs, atp_proof,
                                 outcome)))
-              | maybe_run_slice _ result = result
+              | maybe_run_slice _ _ result = result
           in
             ((Symtab.empty, [], Vector.fromList []),
              ("", SOME 0, [], SOME InternalError))
-            |> fold maybe_run_slice actual_slices
+            |> fold (maybe_run_slice type_sys) actual_slices
+               (* The ATP found an unsound proof? Automatically try again with
+                  full types! *)
+            |> (fn result as (_, (_, _, _, SOME UnsoundProof)) =>
+                   result |> fold (maybe_run_slice (Tags true)) actual_slices
+                 | result => result)
           end
         else
           error ("Bad executable: " ^ Path.print command ^ ".")