# HG changeset patch
# User blanchet
# Date 1284455243 -7200
# Node ID 1ccc5c9ee343c9ab1f92a3e79fa37285b47ba9c2
# Parent  104a6d9e493edb1c4bb1ec480a2a524b21e8e19c
tuning

diff -r 104a6d9e493e -r 1ccc5c9ee343 src/HOL/Tools/Sledgehammer/metis_tactics.ML
--- 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) =