src/HOL/Library/Sum_of_Squares/sos_wrapper.ML

--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Thu Jul 18 13:12:54 2013 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Thu Jul 18 20:53:22 2013 +0200
@@ -130,7 +130,7 @@
 
 fun output_line cert =
   "To repeat this proof with a certifiate use this command:\n" ^
-    Active.sendback_markup ("by (sos_cert \"" ^ cert ^ "\")")
+    Active.sendback_markup [] ("by (sos_cert \"" ^ cert ^ "\")")
 
 val print_cert = warning o output_line o PositivstellensatzTools.pss_tree_to_cert