src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
changeset 59184 830bb7ddb3ab
parent 58631 41333b45bff9
child 62549 9498623b27f0
--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Tue Dec 23 16:00:38 2014 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Tue Dec 23 20:46:42 2014 +0100
@@ -58,7 +58,7 @@
 (* method setup *)
 
 fun print_cert cert =
-  (writeln o Markup.markup Markup.information)
+  Output.information
     ("To repeat this proof with a certificate use this command:\n" ^
       Active.sendback_markup [] ("by (sos \"" ^ Positivstellensatz_Tools.print_cert cert ^ "\")"))