# HG changeset patch
# User blanchet
# Date 1290690828 -3600
# Node ID 77435a7853d1bfa3457406f57e71e320e743dbd4
# Parent  a4171afcc3c49a896f029164cc7e1cad6557fbb8
reverted c059d550afec -- the triviality check had apparently nothing to do with spontaneous Interrupt exceptions

diff -r a4171afcc3c4 -r 77435a7853d1 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Nov 25 13:26:12 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Nov 25 14:13:48 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