src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
changeset 58629 a6a6cd499d4e
parent 58418 a04b242a7a01
child 58630 71cdb885b3bb
--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Wed Oct 08 10:03:46 2014 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Wed Oct 08 10:15:04 2014 +0200
@@ -131,7 +131,7 @@
   "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
+val print_cert = warning o output_line o Positivstellensatz_Tools.print_cert
 
 
 (* method setup *)
@@ -149,7 +149,7 @@
     (Scan.lift Parse.string
       >> (fn cert => fn ctxt =>
         sos_solver ignore
-          (Sum_of_Squares.Certificate (PositivstellensatzTools.cert_to_pss_tree ctxt cert)) ctxt))
+          (Sum_of_Squares.Certificate (Positivstellensatz_Tools.read_cert ctxt cert)) ctxt))
     "prove universal problems over the reals using sums of squares with certificates")
 
 end