# HG changeset patch
# User blanchet
# Date 1325611998 -3600
# Node ID 4d9a5f1514b44adacd799a39efe5b78f9ce6850e
# Parent  4bf24b90703c596d8e580fb6524be1634a6aeaf6
simplify mem Collect

diff -r 4bf24b90703c -r 4d9a5f1514b4 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- 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 _ $ _) =>