Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
changeset 45519 cd6e78cb6ee8
parent 45514 973bb7846505
child 45520 2b1dde0b1c30 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Nov 16 11:16:23 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Nov 16 13:22:36 2011 +0100
@@ -205,7 +205,7 @@
      | {preplay, message, ...} =>
        (NONE, (preplay, prefix "Prover error: " o message, "")))
     handle ERROR msg =>
-           (NONE, (K (Failed_to_Play Metis), fn _ => "Error: " ^ msg, ""))
+           (NONE, (K (Failed_to_Play plain_metis), fn _ => "Error: " ^ msg, ""))
   end
 
 fun run_minimize (params as {provers, ...}) i refs state =
isabelle