made SML/NJ happy
authorboehmes
Wed, 27 Oct 2010 08:58:03 +0200
changeset 40208 54e5e8e0b2a4
parent 40207 5da3e8ede850
child 40209 8ec474f94d61
child 40210 aee7ef725330
made SML/NJ happy
src/HOL/Tools/SMT/smt_setup_solvers.ML
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML	Tue Oct 26 21:51:04 2010 +0200
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML	Wed Oct 27 08:58:03 2010 +0200
@@ -29,7 +29,7 @@
 
 (* CVC3 *)
 
-val cvc3 = {
+fun cvc3 () = {
   name = "cvc3",
   env_var = "CVC3_SOLVER",
   is_remote = true,
@@ -43,7 +43,7 @@
 
 (* Yices *)
 
-val yices = {
+fun yices () = {
   name = "yices",
   env_var = "YICES_SOLVER",
   is_remote = false,
@@ -75,7 +75,7 @@
     |>> outcome_of "unsat" "sat" "unknown" solver_name
   end
 
-val z3 = {
+fun z3 () = {
   name = "z3",
   env_var = "Z3_SOLVER",
   is_remote = true,
@@ -89,8 +89,8 @@
 (* overall setup *)
 
 val setup =
-  SMT_Solver.add_solver cvc3 #>
-  SMT_Solver.add_solver yices #>
-  SMT_Solver.add_solver z3
+  SMT_Solver.add_solver (cvc3 ()) #>
+  SMT_Solver.add_solver (yices ()) #>
+  SMT_Solver.add_solver (z3 ())
 
 end