# HG changeset patch
# User blanchet
# Date 1288097335 -7200
# Node ID 9f82ed60e7ec4793b1a998fc43911ec9ae338bc6
# Parent  fe4a58419d46845acf61f901a98cb2507a3e8f7e
tuning

diff -r fe4a58419d46 -r 9f82ed60e7ec src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Oct 26 14:11:34 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Tue Oct 26 14:48:55 2010 +0200
@@ -425,7 +425,8 @@
                          (apply_on_subgoal subgoal subgoal_count ^
                           command_call smtN (map fst used_facts)) ^
         minimize_line minimize_command (map fst used_facts)
-      | SOME (SMT_Solver.Other_Failure message) => message
+      | SOME (failure as SMT_Solver.Other_Failure _) =>
+        SMT_Solver.string_of_failure ctxt failure
       | SOME _ => string_for_failure (the outcome')
   in
     {outcome = outcome', used_axioms = used_facts,