# HG changeset patch
# User blanchet
# Date 1297350333 -3600
# Node ID 4b3edd6a375d3a5e1dc51537140073c0332fe94a
# Parent  a18e7bbca258be6c697de74de1ef379702735067
remove pointless clutter

diff -r a18e7bbca258 -r 4b3edd6a375d src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Feb 10 10:09:38 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Feb 10 16:05:33 2011 +0100
@@ -30,11 +30,6 @@
 
 (* wrapper for calling external prover *)
 
-fun short_string_for_failure ATP_Proof.Unprovable = "Unprovable."
-  | short_string_for_failure ATP_Proof.TimedOut = "Timed out."
-  | short_string_for_failure ATP_Proof.Interrupted = "Interrupted."
-  | short_string_for_failure _ = "Error."
-
 fun n_facts names =
   let val n = length names in
     string_of_int n ^ " fact" ^ plural_s n ^
@@ -81,12 +76,9 @@
   in
     print silent (fn () =>
         case outcome of
-          SOME failure =>
-          (if verbose then string_for_failure else short_string_for_failure)
-              failure
-        | NONE =>
-          if length used_facts = length facts then "Found proof."
-          else "Found proof with " ^ n_facts used_facts ^ ".");
+          SOME failure => string_for_failure failure
+        | NONE => if length used_facts = length facts then "Found proof."
+                  else "Found proof with " ^ n_facts used_facts ^ ".");
     result
   end