simplify mem Collect
authorblanchet
Tue Jan 03 18:33:18 2012 +0100 (2012-01-03)
changeset 460944d9a5f1514b4
parent 46093 4bf24b90703c
child 46095 cd5c72462bca
simplify mem Collect
src/HOL/Tools/Nitpick/nitpick_hol.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jan 03 18:33:18 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Jan 03 18:33:18 2012 +0100
     1.3 @@ -1661,6 +1661,8 @@
     1.4            do_term depth Ts
     1.5                    (Const (@{const_name prod}, T1 --> range_type T2 --> T3)
     1.6                     $ t1 $ incr_boundvars ~1 t2')
     1.7 +      | Const (@{const_name Set.member}, _) $ t1
     1.8 +        $ (Const (@{const_name Collect}, _) $ t2) => do_term depth Ts (t2 $ t1)
     1.9        | Const (x as (@{const_name distinct},
    1.10                 Type (@{type_name fun}, [Type (@{type_name list}, [T']), _])))
    1.11          $ (t1 as _ $ _) =>