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