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.
merged
authornipkow
Thu, 25 Nov 2010 14:36:51 +0100
changeset 40696 88b9f93d9009
parent 40694 77435a7853d1 (diff)
parent 40695 1b2573c3b222 (current diff)
child 40699 af30b8875733
merged
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Nov 25 14:35:52 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Nov 25 14:36:51 2010 +0100
@@ -526,12 +526,10 @@
       val (prover_name, _) = get_prover ctxt args
       val minimize = AList.defined (op =) args minimizeK
       val metis_ft = AList.defined (op =) args metis_ftK
-      val trivial = false
-(* FIXME
+      val trivial =
        TimeLimit.timeLimit try_outer_timeout
                                    (Try.invoke_try (SOME try_inner_timeout)) pre
                     handle TimeLimit.TimeOut => false
-*)
       fun apply_reconstructor m1 m2 =
         if metis_ft
         then
isabelle