src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 58843 521cea5fa777
parent 58634 9f10d82e8188
child 59058 a78612c67ec0
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Oct 31 11:18:17 2014 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Oct 31 11:36:41 2014 +0100
     1.3 @@ -1059,7 +1059,7 @@
     1.4            if debug then
     1.5              (if negate then "Genuineness" else "Spuriousness") ^ " goal: " ^
     1.6              Syntax.string_of_term ctxt prop ^ "."
     1.7 -            |> Output.urgent_message
     1.8 +            |> writeln
     1.9            else
    1.10              ()
    1.11          val goal = prop |> cterm_of thy |> Goal.init