1.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Jun 01 17:45:28 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Jun 01 17:51:41 2010 +0200
     1.3 @@ -25,6 +25,10 @@
     1.4    (polar = Pos andalso quant_s = @{const_name Ex}) orelse
     1.5    (polar = Neg andalso quant_s <> @{const_name Ex})
     1.6  
     1.7 +val is_descr =
     1.8 +  member (op =) [@{const_name The}, @{const_name Eps}, @{const_name safe_The},
     1.9 +                 @{const_name safe_Eps}]
    1.10 +
    1.11  (** Binary coding of integers **)
    1.12  
    1.13  (* If a formula contains a numeral whose absolute value is more than this
    1.14 @@ -179,7 +183,7 @@
    1.15          list_comb (Const (s0, T --> T --> body_type T0),
    1.16                     map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2])
    1.17        end
    1.18 -    and do_description_operator s T =
    1.19 +    and do_descr s T =
    1.20        let val T1 = box_type hol_ctxt InFunLHS (range_type T) in
    1.21          Const (s, (T1 --> bool_T) --> T1)
    1.22        end
    1.23 @@ -214,27 +218,26 @@
    1.24        | @{const "op -->"} $ t1 $ t2 =>
    1.25          @{const "op -->"} $ do_term new_Ts old_Ts (flip_polarity polar) t1
    1.26          $ do_term new_Ts old_Ts polar t2
    1.27 -      | Const (s as @{const_name The}, T) => do_description_operator s T
    1.28 -      | Const (s as @{const_name Eps}, T) => do_description_operator s T
    1.29 -      | Const (s as @{const_name safe_The}, T) => do_description_operator s T
    1.30 -      | Const (s as @{const_name safe_Eps}, T) => do_description_operator s T
    1.31        | Const (x as (s, T)) =>
    1.32 -        Const (s, if s = @{const_name converse} orelse
    1.33 -                     s = @{const_name trancl} then
    1.34 -                    box_relational_operator_type T
    1.35 -                  else if String.isPrefix quot_normal_prefix s then
    1.36 -                    let val T' = box_type hol_ctxt InFunLHS (domain_type T) in
    1.37 -                      T' --> T'
    1.38 -                    end
    1.39 -                  else if is_built_in_const thy stds fast_descrs x orelse
    1.40 -                          s = @{const_name Sigma} then
    1.41 -                    T
    1.42 -                  else if is_constr_like ctxt x then
    1.43 -                    box_type hol_ctxt InConstr T
    1.44 -                  else if is_sel s orelse is_rep_fun ctxt x then
    1.45 -                    box_type hol_ctxt InSel T
    1.46 -                  else
    1.47 -                    box_type hol_ctxt InExpr T)
    1.48 +        if is_descr s then
    1.49 +          do_descr s T
    1.50 +        else
    1.51 +          Const (s, if s = @{const_name converse} orelse
    1.52 +                       s = @{const_name trancl} then
    1.53 +                      box_relational_operator_type T
    1.54 +                    else if String.isPrefix quot_normal_prefix s then
    1.55 +                      let val T' = box_type hol_ctxt InFunLHS (domain_type T) in
    1.56 +                        T' --> T'
    1.57 +                      end
    1.58 +                    else if is_built_in_const thy stds fast_descrs x orelse
    1.59 +                            s = @{const_name Sigma} then
    1.60 +                      T
    1.61 +                    else if is_constr_like ctxt x then
    1.62 +                      box_type hol_ctxt InConstr T
    1.63 +                    else if is_sel s orelse is_rep_fun ctxt x then
    1.64 +                      box_type hol_ctxt InSel T
    1.65 +                    else
    1.66 +                      box_type hol_ctxt InExpr T)
    1.67        | t1 $ Abs (s, T, t2') =>
    1.68          let
    1.69            val t1 = do_term new_Ts old_Ts Neut t1
    1.70 @@ -924,6 +927,9 @@
    1.71                 end
    1.72               else if is_constr ctxt stds x then
    1.73                 accum
    1.74 +             else if is_descr (original_name s) then
    1.75 +               fold (add_nondef_axiom depth) (equational_fun_axioms hol_ctxt x)
    1.76 +                    accum
    1.77               else if is_equational_fun hol_ctxt x then
    1.78                 fold (add_eq_axiom depth) (equational_fun_axioms hol_ctxt x)
    1.79                      accum