# HG changeset patch
# User blanchet
# Date 1335253660 -7200
# Node ID dc9c8ce4aac56654ed0694476cc3af993b777081
# Parent  04400144c6fc1b7a3e29467b54e524794742c373
add a timeout on the monotonicity check

diff -r 04400144c6fc -r dc9c8ce4aac5 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Apr 24 09:47:40 2012 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Apr 24 09:47:40 2012 +0200
@@ -383,7 +383,9 @@
        (not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
       is_number_type ctxt T orelse is_bit_type T
     fun is_type_actually_monotonic T =
-      formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
+      time_limit tac_timeout (formulas_monotonic hol_ctxt binarize T)
+                 (nondef_ts, def_ts)
+      handle TimeLimit.TimeOut => false
     fun is_type_kind_of_monotonic T =
       case triple_lookup (type_match thy) monos T of
         SOME (SOME false) => false