src/HOL/Tools/Nitpick/nitpick_hol.ML
changeset 46102 b669437de253
parent 46101 da17bfdadef6
child 46107 e740ffcd0ef4
     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,8 +1661,6 @@
     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 _ $ _) =>