src/HOL/Tools/Nitpick/nitpick.ML
changeset 47716 dc9c8ce4aac5
parent 47715 04400144c6fc
child 47745 de249b5ae6e2
child 47752 0814fc93ab89
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Apr 24 09:47:40 2012 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Apr 24 09:47:40 2012 +0200
     1.3 @@ -383,7 +383,9 @@
     1.4         (not (is_pure_typedef ctxt T) orelse is_univ_typedef ctxt T)) orelse
     1.5        is_number_type ctxt T orelse is_bit_type T
     1.6      fun is_type_actually_monotonic T =
     1.7 -      formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
     1.8 +      time_limit tac_timeout (formulas_monotonic hol_ctxt binarize T)
     1.9 +                 (nondef_ts, def_ts)
    1.10 +      handle TimeLimit.TimeOut => false
    1.11      fun is_type_kind_of_monotonic T =
    1.12        case triple_lookup (type_match thy) monos T of
    1.13          SOME (SOME false) => false