# HG changeset patch
# User blanchet
# Date 1325611998 -3600
# Node ID b669437de253b77e94f1eeafdce8e5274abde672
# Parent  da17bfdadef67f2af1190d17c34d32d9a42a0471
more robust destruction of "set Collect" idiom

diff -r da17bfdadef6 -r b669437de253 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,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 _ $ _) =>
diff -r da17bfdadef6 -r b669437de253 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- 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