# HG changeset patch
# User boehmes
# Date 1288162683 -7200
# Node ID 54e5e8e0b2a45603c769297fbb5599635edb459d
# Parent  5da3e8ede850817f7fc5a36f99a56edcca360879
made SML/NJ happy

diff -r 5da3e8ede850 -r 54e5e8e0b2a4 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