# HG changeset patch
# User blanchet
# Date 1292408788 -3600
# Node ID 43e2b051339c51f87836b18581881e3d999e8faf
# Parent  ad923cdd4a5d9e625e6851b83216a5d6520945f3
weaken the "expect" flag so that it doesn't trigger errors if a prover is not installed

diff -r ad923cdd4a5d -r 43e2b051339c src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Dec 15 11:26:28 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Wed Dec 15 11:26:28 2010 +0100
@@ -86,7 +86,11 @@
                       ("unknown", "Internal error:\n" ^
                                   ML_Compiler.exn_message exn ^ "\n"))
         val _ =
-          if expect = "" orelse outcome_code = expect then
+          (* The "expect" argument is deliberately ignored if the prover is
+             missing so that the "Metis_Examples" can be processed on any
+             machine. *)
+          if expect = "" orelse outcome_code = expect orelse
+             not (is_prover_installed ctxt name) then
             ()
           else if blocking then
             error ("Unexpected outcome: " ^ quote outcome_code ^ ".")