src/HOL/Library/Sum_of_Squares/sos_wrapper.ML
changeset 42616 92715b528e78
parent 41950 134131d519c0
child 43850 7f2cbc713344
--- a/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Mon May 02 13:29:47 2011 +0200
+++ b/src/HOL/Library/Sum_of_Squares/sos_wrapper.ML	Mon May 02 16:33:21 2011 +0200
@@ -24,7 +24,7 @@
 
 (*** calling provers ***)
 
-val (dest_dir, setup_dest_dir) = Attrib.config_string "sos_dest_dir" (K "")
+val dest_dir = Attrib.setup_config_string @{binding sos_dest_dir} (K "")
 
 fun filename dir name =
   let
@@ -117,7 +117,7 @@
   | prover "csdp" = csdp
   | prover name = error ("Unknown prover: " ^ name)
 
-val (prover_name, setup_prover_name) = Attrib.config_string "sos_prover_name" (K "remote_csdp")
+val prover_name = Attrib.setup_config_string @{binding sos_prover_name} (K "remote_csdp")
 
 fun call_solver ctxt opt_name =
   let
@@ -140,8 +140,6 @@
 fun sos_solver print method = SIMPLE_METHOD' o Sum_of_Squares.sos_tac print method
 
 val setup =
-  setup_dest_dir #>
-  setup_prover_name #>
   Method.setup @{binding sos}
     (Scan.lift (Scan.option Parse.xname)
       >> (fn opt_name => fn ctxt =>