changeset 40132 | 7ee65dbffa31 |
parent 39687 | 4e9b6ada3a21 |
child 41045 | 2a41709f34c1 |
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Oct 25 20:24:13 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Mon Oct 25 21:06:56 2010 +0200 @@ -2054,7 +2054,7 @@ map (wf_constraint_for_triple rel) triples |> foldr1 s_conj |> HOLogic.mk_Trueprop val _ = if debug then - priority ("Wellfoundedness goal: " ^ + Output.urgent_message ("Wellfoundedness goal: " ^ Syntax.string_of_term ctxt prop ^ ".") else ()