src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
changeset 58418 a04b242a7a01
parent 56625 54505623a8ef
child 58629 a6a6cd499d4e
--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Mon Sep 22 10:55:51 2014 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Mon Sep 22 16:15:29 2014 +0200
@@ -7,7 +7,6 @@
 signature SOS_WRAPPER =
 sig
   datatype prover_result = Success | Failure | Error
-  val setup: theory -> theory
   val dest_dir: string Config.T
   val prover_name: string Config.T
 end
@@ -139,8 +138,8 @@
 
 fun sos_solver print method = SIMPLE_METHOD' o Sum_of_Squares.sos_tac print method
 
-val setup =
-  Method.setup @{binding sos}
+val _ = Theory.setup
+ (Method.setup @{binding sos}
     (Scan.lift (Scan.option Parse.xname)
       >> (fn opt_name => fn ctxt =>
         sos_solver print_cert
@@ -151,6 +150,6 @@
       >> (fn cert => fn ctxt =>
         sos_solver ignore
           (Sum_of_Squares.Certificate (PositivstellensatzTools.cert_to_pss_tree ctxt cert)) ctxt))
-    "prove universal problems over the reals using sums of squares with certificates"
+    "prove universal problems over the reals using sums of squares with certificates")
 
 end