# HG changeset patch
# User blanchet
# Date 1291639605 -3600
# Node ID 83f241623b86632816b570a6e744b4567659ee75
# Parent  666d8ed0b73a627894f41cf1dff1bfb59b6f6cd3
fix monotonicity type of None

diff -r 666d8ed0b73a -r 83f241623b86 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:36:28 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:46:45 2010 +0100
@@ -848,8 +848,8 @@
        case t of
          @{const False} =>
          (MRaw (t, bool_M), accum ||> add_comp_frame (A Fls) Leq frame)
-       | Const (@{const_name None}, _) =>
-         (MRaw (t, bool_M), accum ||> add_comp_frame (A Fls) Leq frame)
+       | Const (@{const_name None}, T) =>
+         (MRaw (t, mtype_for T), accum ||> add_comp_frame (A Fls) Leq frame)
        | @{const True} =>
          (MRaw (t, bool_M), accum ||> add_comp_frame (A Tru) Leq frame)
        | (t0 as Const (@{const_name HOL.eq}, _)) $ Bound 0 $ t2 =>