# HG changeset patch
# User blanchet
# Date 1300439857 -3600
# Node ID c567c860caf67803765d5569eddabbffaa3e4db3
# Parent  bd6296de14327b3d77d0e0d4c3437b93f35a5555
always destroy constructor patterns, since this seems to be always useful

diff -r bd6296de1432 -r c567c860caf6 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Mar 17 22:07:17 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Mar 18 10:17:37 2011 +0100
@@ -214,6 +214,7 @@
   val fixpoint_kind_of_const :
     theory -> const_table * const_table -> string * typ -> fixpoint_kind
   val is_real_inductive_pred : hol_context -> styp -> bool
+  val is_constr_pattern : Proof.context -> term -> bool
   val is_constr_pattern_lhs : Proof.context -> term -> bool
   val is_constr_pattern_formula : Proof.context -> term -> bool
   val nondef_props_for_const :
diff -r bd6296de1432 -r c567c860caf6 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Mar 17 22:07:17 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Fri Mar 18 10:17:37 2011 +0100
@@ -387,7 +387,7 @@
           (list_comb (t, args), seen)
   in aux [] 0 t [] [] |> fst end
 
-fun destroy_pulled_out_constrs (hol_ctxt as {ctxt, stds, ...}) axiom t =
+fun destroy_pulled_out_constrs (hol_ctxt as {ctxt, stds, ...}) axiom strong t =
   let
     val num_occs_of_var =
       fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
@@ -404,7 +404,8 @@
       | aux Ts careful (t1 $ t2) = aux Ts careful t1 $ aux Ts careful t2
       | aux _ _ t = t
     and aux_eq Ts careful pass1 t0 t1 t2 =
-      ((if careful then
+      ((if careful orelse
+           not (strong orelse forall (is_constr_pattern ctxt) [t1, t2]) then
           raise SAME ()
         else if axiom andalso is_Var t2 andalso
                 num_occs_of_var (dest_Var t2) = 1 then
@@ -1270,8 +1271,8 @@
       #> 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_pulled_out_constrs hol_ctxt def)
+                         #> pull_out_existential_constrs hol_ctxt)
+      #> destroy_pulled_out_constrs hol_ctxt def destroy_constrs
       #> curry_assms
       #> destroy_universal_equalities
       #> destroy_existential_equalities hol_ctxt