# HG changeset patch
# User blanchet
# Date 1290550213 -3600
# Node ID c059d550afecd98c6c8df00333d8a8724f7b814f
# Parent  5c316d1327d462ab5a4281d679fd3f79d4e4fd3a
disable triviality checking -- it might be the source of the spurious Interrupt exceptions that make it almost impossible to run Judgement Day

diff -r 5c316d1327d4 -r c059d550afec src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Nov 23 22:37:16 2010 +0100
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Tue Nov 23 23:10:13 2010 +0100
@@ -526,9 +526,12 @@
       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 = TimeLimit.timeLimit try_outer_timeout
+      val trivial = false
+(* FIXME
+       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