src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
changeset 45666 d83797ef0d2d
parent 43850 7f2cbc713344
child 50163 c62ce309dc26
--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Mon Nov 28 20:39:08 2011 +0100
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Mon Nov 28 22:05:32 2011 +0100
@@ -130,7 +130,7 @@
 
 fun output_line cert =
   "To repeat this proof with a certifiate use this command:\n" ^
-    Markup.markup Markup.sendback ("by (sos_cert \"" ^ cert ^ "\")")
+    Markup.markup Isabelle_Markup.sendback ("by (sos_cert \"" ^ cert ^ "\")")
 
 val print_cert = warning o output_line o PositivstellensatzTools.pss_tree_to_cert