src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 41018 83f241623b86
parent 41017 666d8ed0b73a
child 41049 0edd245892ed
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:36:28 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:46:45 2010 +0100
     1.3 @@ -848,8 +848,8 @@
     1.4         case t of
     1.5           @{const False} =>
     1.6           (MRaw (t, bool_M), accum ||> add_comp_frame (A Fls) Leq frame)
     1.7 -       | Const (@{const_name None}, _) =>
     1.8 -         (MRaw (t, bool_M), accum ||> add_comp_frame (A Fls) Leq frame)
     1.9 +       | Const (@{const_name None}, T) =>
    1.10 +         (MRaw (t, mtype_for T), accum ||> add_comp_frame (A Fls) Leq frame)
    1.11         | @{const True} =>
    1.12           (MRaw (t, bool_M), accum ||> add_comp_frame (A Tru) Leq frame)
    1.13         | (t0 as Const (@{const_name HOL.eq}, _)) $ Bound 0 $ t2 =>