src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
changeset 52697 6fb98a20c349
parent 50450 358b6020f8b6
child 56625 54505623a8ef
     1.1 --- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Thu Jul 18 13:12:54 2013 +0200
     1.2 +++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Thu Jul 18 20:53:22 2013 +0200
     1.3 @@ -130,7 +130,7 @@
     1.4  
     1.5  fun output_line cert =
     1.6    "To repeat this proof with a certifiate use this command:\n" ^
     1.7 -    Active.sendback_markup ("by (sos_cert \"" ^ cert ^ "\")")
     1.8 +    Active.sendback_markup [] ("by (sos_cert \"" ^ cert ^ "\")")
     1.9  
    1.10  val print_cert = warning o output_line o PositivstellensatzTools.pss_tree_to_cert
    1.11