diff -r ec83638b6bfb -r 830bb7ddb3ab src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
--- 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 ^ "\")"))