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.
give more helpful error message
authorblanchet
Wed, 02 Jun 2010 12:28:42 +0200
changeset 37318 32b3d16b04f6
parent 37277 87988eeed572
child 37319 42268dc7d6c4
give more helpful error message
src/HOL/Tools/Sledgehammer/metis_tactics.ML file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle