src/HOL/Tools/Nitpick/nitpick_hol.ML
 changeset 41871 394eef237bd1 parent 41860 49d0fc8c418c child 41875 e3cd0dce9b1a
```     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Mar 02 13:09:57 2011 +0100
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Mar 02 14:50:16 2011 +0100
1.3 @@ -27,6 +27,7 @@
1.4       destroy_constrs: bool,
1.5       specialize: bool,
1.6       star_linear_preds: bool,
1.7 +     total_consts: bool option,
1.8       preconstrs: (term option * bool option) list,
1.9       tac_timeout: Time.time option,
1.10       evals: term list,
1.11 @@ -259,6 +260,7 @@
1.12     destroy_constrs: bool,
1.13     specialize: bool,
1.14     star_linear_preds: bool,
1.15 +   total_consts: bool option,
1.16     preconstrs: (term option * bool option) list,
1.17     tac_timeout: Time.time option,
1.18     evals: term list,
1.19 @@ -1634,13 +1636,15 @@
1.20  val unfold_max_depth = 255
1.21
1.22  (* Inline definitions or define as an equational constant? Booleans tend to
1.23 -   benefit more from inlining, due to the polarity analysis. *)
1.24 +   benefit more from inlining, due to the polarity analysis. (However, if
1.25 +   "total_consts" is set, the polarity analysis is likely not to be so
1.26 +   crucial.) *)
1.27  val def_inline_threshold_for_booleans = 60
1.28  val def_inline_threshold_for_non_booleans = 20
1.29
1.30  fun unfold_defs_in_term
1.31 -        (hol_ctxt as {thy, ctxt, stds, whacks, case_names, def_tables,
1.32 -                      ground_thm_table, ersatz_table, ...}) =
1.33 +        (hol_ctxt as {thy, ctxt, stds, whacks, total_consts, case_names,
1.34 +                      def_tables, ground_thm_table, ersatz_table, ...}) =
1.35    let
1.36      fun do_term depth Ts t =
1.37        case t of
1.38 @@ -1718,7 +1722,8 @@
1.39        | NONE =>
1.40          let
1.41            fun def_inline_threshold () =
1.42 -            if is_boolean_type (nth_range_type (length ts) T) then
1.43 +            if is_boolean_type (nth_range_type (length ts) T) andalso
1.44 +               total_consts <> SOME true then
1.45                def_inline_threshold_for_booleans
1.46              else
1.47                def_inline_threshold_for_non_booleans
```