diff -r 87988eeed572 -r 32b3d16b04f6 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Jun 02 11:53:17 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Wed Jun 02 12:28:42 2010 +0200
@@ -409,9 +409,10 @@
           (substs' |> map (fn (x, y) =>
             Syntax.string_of_term ctxt (term_of x) ^ " |-> " ^
             Syntax.string_of_term ctxt (term_of y)))));
-  in  cterm_instantiate substs' i_th
-      handle THM (msg, _, _) => error ("metis error (inst_inf): " ^ msg)
-  end;
+  in  cterm_instantiate substs' i_th end
+  handle THM (msg, _, _) => error ("metis error (inst_inf):\n" ^ msg)
+       | ERROR msg => error ("metis error (inst_inf):\n" ^ msg ^
+                             "\n(Perhaps you want to try \"metisFT\".)")
 
 (* INFERENCE RULE: RESOLVE *)