Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tuning
authorblanchet
Tue, 26 Oct 2010 14:48:55 +0200
changeset 40190 9f82ed60e7ec
parent 40186 fe4a58419d46
child 40191 257d2e06bfb8
tuning
src/HOL/Tools/Sledgehammer/sledgehammer.ML file | annotate | diff | comparison | revisions 
--- 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,
isabelle