diff -r a14a492f472f -r 394eef237bd1 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Mar 02 13:09:57 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Mar 02 14:50:16 2011 +0100
@@ -27,6 +27,7 @@
      destroy_constrs: bool,
      specialize: bool,
      star_linear_preds: bool,
+     total_consts: bool option,
      preconstrs: (term option * bool option) list,
      tac_timeout: Time.time option,
      evals: term list,
@@ -259,6 +260,7 @@
    destroy_constrs: bool,
    specialize: bool,
    star_linear_preds: bool,
+   total_consts: bool option,
    preconstrs: (term option * bool option) list,
    tac_timeout: Time.time option,
    evals: term list,
@@ -1634,13 +1636,15 @@
 val unfold_max_depth = 255
 
 (* Inline definitions or define as an equational constant? Booleans tend to
-   benefit more from inlining, due to the polarity analysis. *)
+   benefit more from inlining, due to the polarity analysis. (However, if
+   "total_consts" is set, the polarity analysis is likely not to be so
+   crucial.) *)
 val def_inline_threshold_for_booleans = 60
 val def_inline_threshold_for_non_booleans = 20
 
 fun unfold_defs_in_term
-        (hol_ctxt as {thy, ctxt, stds, whacks, case_names, def_tables,
-                      ground_thm_table, ersatz_table, ...}) =
+        (hol_ctxt as {thy, ctxt, stds, whacks, total_consts, case_names,
+                      def_tables, ground_thm_table, ersatz_table, ...}) =
   let
     fun do_term depth Ts t =
       case t of
@@ -1718,7 +1722,8 @@
       | NONE =>
         let
           fun def_inline_threshold () =
-            if is_boolean_type (nth_range_type (length ts) T) then
+            if is_boolean_type (nth_range_type (length ts) T) andalso
+               total_consts <> SOME true then
               def_inline_threshold_for_booleans
             else
               def_inline_threshold_for_non_booleans