diff -r 31e75ad9ae17 -r 9dd0a2f83429 src/HOL/Tools/Function/scnp_solve.ML
--- 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