--- 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 =>