# HG changeset patch
# User blanchet
# Date 1275407501 -7200
# Node ID 694aebcd602b3cf24c630fc7240c04894c63bfe2
# Parent  c0f36d44de3339a086bc55c5549724709fef8c7b
fix Nitpick soundness bug regarding The and Eps

diff -r c0f36d44de33 -r 694aebcd602b src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Jun 01 17:45:28 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Jun 01 17:51:41 2010 +0200
@@ -25,6 +25,10 @@
   (polar = Pos andalso quant_s = @{const_name Ex}) orelse
   (polar = Neg andalso quant_s <> @{const_name Ex})
 
+val is_descr =
+  member (op =) [@{const_name The}, @{const_name Eps}, @{const_name safe_The},
+                 @{const_name safe_Eps}]
+
 (** Binary coding of integers **)
 
 (* If a formula contains a numeral whose absolute value is more than this
@@ -179,7 +183,7 @@
         list_comb (Const (s0, T --> T --> body_type T0),
                    map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2])
       end
-    and do_description_operator s T =
+    and do_descr s T =
       let val T1 = box_type hol_ctxt InFunLHS (range_type T) in
         Const (s, (T1 --> bool_T) --> T1)
       end
@@ -214,27 +218,26 @@
       | @{const "op -->"} $ t1 $ t2 =>
         @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
         $ do_term new_Ts old_Ts polar t2
-      | Const (s as @{const_name The}, T) => do_description_operator s T
-      | Const (s as @{const_name Eps}, T) => do_description_operator s T
-      | Const (s as @{const_name safe_The}, T) => do_description_operator s T
-      | Const (s as @{const_name safe_Eps}, T) => do_description_operator s T
       | Const (x as (s, T)) =>
-        Const (s, if s = @{const_name converse} orelse
-                     s = @{const_name trancl} then
-                    box_relational_operator_type T
-                  else if String.isPrefix quot_normal_prefix s then
-                    let val T' = box_type hol_ctxt InFunLHS (domain_type T) in
-                      T' --> T'
-                    end
-                  else if is_built_in_const thy stds fast_descrs x orelse
-                          s = @{const_name Sigma} then
-                    T
-                  else if is_constr_like ctxt x then
-                    box_type hol_ctxt InConstr T
-                  else if is_sel s orelse is_rep_fun ctxt x then
-                    box_type hol_ctxt InSel T
-                  else
-                    box_type hol_ctxt InExpr T)
+        if is_descr s then
+          do_descr s T
+        else
+          Const (s, if s = @{const_name converse} orelse
+                       s = @{const_name trancl} then
+                      box_relational_operator_type T
+                    else if String.isPrefix quot_normal_prefix s then
+                      let val T' = box_type hol_ctxt InFunLHS (domain_type T) in
+                        T' --> T'
+                      end
+                    else if is_built_in_const thy stds fast_descrs x orelse
+                            s = @{const_name Sigma} then
+                      T
+                    else if is_constr_like ctxt x then
+                      box_type hol_ctxt InConstr T
+                    else if is_sel s orelse is_rep_fun ctxt x then
+                      box_type hol_ctxt InSel T
+                    else
+                      box_type hol_ctxt InExpr T)
       | t1 $ Abs (s, T, t2') =>
         let
           val t1 = do_term new_Ts old_Ts Neut t1
@@ -924,6 +927,9 @@
                end
              else if is_constr ctxt stds x then
                accum
+             else if is_descr (original_name s) then
+               fold (add_nondef_axiom depth) (equational_fun_axioms hol_ctxt x)
+                    accum
              else if is_equational_fun hol_ctxt x then
                fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
                     accum