src/HOL/Library/Sum_of_Squares/sos_wrapper.ML

 (* method setup *)
 
 fun print_cert cert =
   Output.information
     ("To repeat this proof with a certificate use this command:\n" ^
-      Active.sendback_markup [Markup.padding_command]
+      Active.sendback_markup_command
         ("by (sos \"" ^ Positivstellensatz_Tools.print_cert cert ^ "\")"))
 
 fun sos_tac ctxt NONE =
       Sum_of_Squares.sos_tac print_cert
         (Sum_of_Squares.Prover (run_solver ctxt)) ctxt