diff -r 7eed0fee0241 -r 54505623a8ef src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Sat Apr 19 20:01:26 2014 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Sun Apr 20 00:25:05 2014 +0100
@@ -129,8 +129,8 @@
 (* certificate output *)
 
 fun output_line cert =
-  "To repeat this proof with a certifiate use this command:\n" ^
-    Active.sendback_markup [] ("by (sos_cert \"" ^ cert ^ "\")")
+  "To repeat this proof with a certificate use this command:\n" ^
+    Active.sendback_markup [] ("apply (sos_cert \"" ^ cert ^ "\")")
 
 val print_cert = warning o output_line o PositivstellensatzTools.pss_tree_to_cert