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.
compile
authorblanchet
Tue, 29 Jun 2010 11:20:05 +0200
changeset 37631 16048a884a2c
parent 37630 d30930f58006
child 37632 df12f798df99
compile
src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Jun 29 11:14:52 2010 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Jun 29 11:20:05 2010 +0200
@@ -324,7 +324,7 @@
       NONE => (message, SH_OK (time_isa, time_atp, relevant_thm_names))
     | SOME _ => (message, SH_FAIL (time_isa, time_atp))
   end
-  handle Metis_Clauses.TRIVIAL () => ("trivial", SH_OK (0, 0, []))
+  handle ATP_Manager.TRIVIAL () => ("trivial", SH_OK (0, 0, []))
        | ERROR msg => ("error: " ^ msg, SH_ERROR)
        | TimeLimit.TimeOut => ("timeout", SH_ERROR)
isabelle