# HG changeset patch
# User blanchet
# Date 1304267844 -7200
# Node ID e155be7125bacfbd8acfd3e59732d173fee9b060
# Parent  cd99d6d3027a1a90ae30f1a033f17e04f010f46e
added a hint to Metis errors suggesting metisFT -- it sometimes work

diff -r cd99d6d3027a -r e155be7125ba src/HOL/Tools/Metis/metis_tactics.ML
--- a/src/HOL/Tools/Metis/metis_tactics.ML	Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Metis/metis_tactics.ML	Sun May 01 18:37:24 2011 +0200
@@ -160,6 +160,10 @@
       Meson.MESON (preskolem_tac ctxt) (maps neg_clausify)
                   (fn cls => resolve_tac (FOL_SOLVE mode ctxt cls ths) 1)
                   ctxt i st0
+      handle ERROR message =>
+             error (message |> mode <> FT
+                               ? suffix "\nHint: You might want to try out \
+                                        \\"metisFT\".")
   end
 
 val metis_tac = generic_metis_tac HO