src/HOL/Tools/Nitpick/nitpick.ML

                    \efficiently."
                  else
                    "\" could not be proved well-founded. Nitpick might need to \
                    \unroll it.")))
     val _ = if verbose then List.app print_wf (!wf_cache) else ()
+    val das_wort_formula = if falsify then "Negated conjecture" else "Formula"
     val _ =
       pprint_d (fn () => Pretty.chunks
-          (pretties_for_formulas ctxt "Preprocessed formula" [hd nondef_ts] @
+          (pretties_for_formulas ctxt das_wort_formula [hd nondef_ts] @
            pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @
            pretties_for_formulas ctxt "Relevant nondefinitional axiom"
                                  (tl nondef_ts)))
     val _ = List.app (ignore o Term.type_of) (nondef_ts @ def_ts)
             handle TYPE (_, Ts, ts) =>