# HG changeset patch
# User blanchet
# Date 1276541316 -7200
# Node ID c02bd0bb276d2beec1bcbd53daa5d28f11c17c35
# Parent  0714ece4908179280985209ecc5d5fbd48ca7d0e
missing case

diff -r 0714ece49081 -r c02bd0bb276d src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Mon Jun 14 20:16:36 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML	Mon Jun 14 20:48:36 2010 +0200
@@ -38,6 +38,7 @@
 (* wrapper for calling external prover *)
 
 fun string_for_failure Unprovable = "Unprovable."
+  | string_for_failure IncompleteUnprovable = "Failed."
   | string_for_failure TimedOut = "Timed out."
   | string_for_failure OutOfResources = "Failed."
   | string_for_failure OldSpass = "Error."