--- 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,8 +1661,6 @@
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 _ $ _) =>
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Jan 03 18:33:18 2012 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Jan 03 18:33:18 2012 +0100
@@ -281,6 +281,16 @@
Abs (s, T, do_term (T :: new_Ts) (T :: old_Ts) Neut t')
in do_term [] [] Pos orig_t end
+(** Destruction of set membership and comprehensions **)
+
+fun destroy_set_Collect (Const (@{const_name Set.member}, _) $ t1
+ $ (Const (@{const_name Collect}, _) $ t2)) =
+ destroy_set_Collect (t2 $ t1)
+ | destroy_set_Collect (t1 $ t2) =
+ destroy_set_Collect t1 $ destroy_set_Collect t2
+ | destroy_set_Collect (Abs (s, T, t')) = Abs (s, T, destroy_set_Collect t')
+ | destroy_set_Collect t = t
+
(** Destruction of constructors **)
val val_var_prefix = nitpick_prefix ^ "v"
@@ -1268,8 +1278,9 @@
#> box ? uncurry_term table
#> box ? box_fun_and_pair_in_term hol_ctxt def
fun do_tail def =
- destroy_constrs ? (pull_out_universal_constrs hol_ctxt def
- #> pull_out_existential_constrs hol_ctxt)
+ destroy_set_Collect
+ #> destroy_constrs ? (pull_out_universal_constrs hol_ctxt def
+ #> pull_out_existential_constrs hol_ctxt)
#> destroy_pulled_out_constrs hol_ctxt def destroy_constrs
#> curry_assms
#> destroy_universal_equalities