--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jan 03 18:33:18 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jan 03 18:33:18 2012 +0100
@@ -1661,6 +1661,8 @@
do_term depth Ts
(Const (@{const_name prod}, T1 --> range_type T2 --> T3)
$ t1 $ incr_boundvars ~1 t2')
+ | Const (@{const_name Set.member}, _) $ t1
+ $ (Const (@{const_name Collect}, _) $ t2) => do_term depth Ts (t2 $ t1)
| Const (x as (@{const_name distinct},
Type (@{type_name fun}, [Type (@{type_name list}, [T']), _])))
$ (t1 as _ $ _) =>