--- a/src/HOL/Tools/Function/scnp_solve.ML Tue Sep 29 14:59:24 2009 +0200
+++ b/src/HOL/Tools/Function/scnp_solve.ML Tue Sep 29 16:24:36 2009 +0200
@@ -23,7 +23,7 @@
val generate_certificate : bool -> label list -> graph_problem -> certificate option
- val solver : string ref
+ val solver : string Unsynchronized.ref
end
structure ScnpSolve : SCNP_SOLVE =
@@ -71,7 +71,7 @@
fun exactly_one n f = iexists n (the_one f n)
(* SAT solving *)
-val solver = ref "auto";
+val solver = Unsynchronized.ref "auto";
fun sat_solver x =
FundefCommon.PROFILE "sat_solving..." (SatSolver.invoke_solver (!solver)) x