# HG changeset patch
# User blanchet
# Date 1259943472 -3600
# Node ID 2380c1dac86ea9f9c1d58e813b85a38abb4ed66c
# Parent  406d8e34a3cf3c0d2afdddf1723bcfbcc0906e45
fix soundness bug in Nitpick's "destroy_constrs" optimization

diff -r 406d8e34a3cf -r 2380c1dac86e src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Dec 04 15:30:36 2009 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Fri Dec 04 17:17:52 2009 +0100
@@ -1,4 +1,4 @@
-(*  Title:      HOL/Nitpick/Tools/nitpick_hol.ML
+(*  Title:      HOL/Tools/Nitpick/nitpick_hol.ML
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2008, 2009
 
@@ -78,6 +78,7 @@
   val mk_flat_tuple : typ -> term list -> term
   val dest_n_tuple : int -> term -> term list
   val instantiate_type : theory -> typ -> typ -> typ -> typ
+  val is_real_datatype : theory -> string -> bool
   val is_codatatype : theory -> typ -> bool
   val is_pure_typedef : theory -> typ -> bool
   val is_univ_typedef : theory -> typ -> bool
@@ -1985,11 +1986,13 @@
     fun do_term Ts def t args seen =
       case t of
         (t0 as Const (@{const_name "=="}, _)) $ t1 $ t2 =>
-        do_eq_or_imp Ts def t0 t1 t2 seen
-      | (t0 as @{const "==>"}) $ t1 $ t2 => do_eq_or_imp Ts def t0 t1 t2 seen
+        do_eq_or_imp Ts true def t0 t1 t2 seen
+      | (t0 as @{const "==>"}) $ t1 $ t2 =>
+        do_eq_or_imp Ts false def t0 t1 t2 seen
       | (t0 as Const (@{const_name "op ="}, _)) $ t1 $ t2 =>
-        do_eq_or_imp Ts def t0 t1 t2 seen
-      | (t0 as @{const "op -->"}) $ t1 $ t2 => do_eq_or_imp Ts def t0 t1 t2 seen
+        do_eq_or_imp Ts true def t0 t1 t2 seen
+      | (t0 as @{const "op -->"}) $ t1 $ t2 =>
+        do_eq_or_imp Ts false def t0 t1 t2 seen
       | Abs (s, T, t') =>
         let val (t', seen) = do_term (T :: Ts) def t' [] seen in
           (list_comb (Abs (s, T, t'), args), seen)
@@ -1999,11 +2002,12 @@
           do_term Ts def t1 (t2 :: args) seen
         end
       | _ => pull_out_constr_comb thy Ts def k 0 t args seen
-    (* typ list -> bool -> term -> term -> term -> term list
+    (* typ list -> bool -> bool -> term -> term -> term -> term list
        -> term * term list *)
-    and do_eq_or_imp Ts def t0 t1 t2 seen =
+    and do_eq_or_imp Ts eq def t0 t1 t2 seen =
       let
-        val (t2, seen) = do_term Ts def t2 [] seen
+        val (t2, seen) = if eq andalso def then (t2, seen)
+                         else do_term Ts false t2 [] seen
         val (t1, seen) = do_term Ts false t1 [] seen
       in (t0 $ t1 $ t2, seen) end
     val (concl, seen) = do_term [] def t [] []