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, 14 Sep 2010 11:07:23 +0200
changeset 39356 1ccc5c9ee343
parent 39355 104a6d9e493e
child 39357 fe84bc307be6
tuning
src/HOL/Tools/Sledgehammer/metis_tactics.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Tue Sep 14 09:12:28 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/metis_tactics.ML	Tue Sep 14 11:07:23 2010 +0200
@@ -406,7 +406,7 @@
                 val t = hol_term_from_metis mode ctxt y
             in  SOME (cterm_of thy (Var v), t)  end
             handle Option =>
-                (trace_msg (fn() => "List.find failed for the variable " ^ x ^
+                (trace_msg (fn() => "\"find_var\" failed for the variable " ^ x ^
                                        " in " ^ Display.string_of_thm ctxt i_th);
                  NONE)
       fun remove_typeinst (a, t) =
isabelle