# HG changeset patch
# User wenzelm
# Date 1256655786 -3600
# Node ID cf8da4f3f92b1e4aee833d9c2ded5ac51c0ca706
# Parent  83322d6686013115331fa7863ac2b98a3718f5dc
more thread-safe access to global refs;

diff -r 83322d668601 -r cf8da4f3f92b src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Tue Oct 27 16:02:43 2009 +0100
+++ b/src/HOL/Tools/sat_funcs.ML	Tue Oct 27 16:03:06 2009 +0100
@@ -346,11 +346,16 @@
 		fold Thm.weaken (rev sorted_clauses) False_thm
 	end
 in
-	case (tracing ("Invoking solver " ^ (!solver)); SatSolver.invoke_solver (!solver) fm) of
+	case
+	  let val the_solver = ! solver
+	  in (tracing ("Invoking solver " ^ the_solver); SatSolver.invoke_solver the_solver fm) end
+	of
 	  SatSolver.UNSATISFIABLE (SOME (clause_table, empty_id)) => (
 		if !trace_sat then
 			tracing ("Proof trace from SAT solver:\n" ^
-				"clauses: " ^ ML_Syntax.print_list (ML_Syntax.print_pair Int.toString (ML_Syntax.print_list Int.toString)) (Inttab.dest clause_table) ^ "\n" ^
+				"clauses: " ^ ML_Syntax.print_list
+				  (ML_Syntax.print_pair Int.toString (ML_Syntax.print_list Int.toString))
+				  (Inttab.dest clause_table) ^ "\n" ^
 				"empty clause: " ^ Int.toString empty_id)
 		else ();
 		if !quick_and_dirty then
@@ -388,8 +393,9 @@
 			val msg = "SAT solver found a countermodel:\n"
 				^ (commas
 					o map (fn (term, idx) =>
-						Syntax.string_of_term_global @{theory} term ^ ": "
-							^ (case assignment idx of NONE => "arbitrary" | SOME true => "true" | SOME false => "false")))
+						Syntax.string_of_term_global @{theory} term ^ ": " ^
+						  (case assignment idx of NONE => "arbitrary"
+							| SOME true => "true" | SOME false => "false")))
 					(Termtab.dest atom_table)
 		in
 			raise THM (msg, 0, [])
diff -r 83322d668601 -r cf8da4f3f92b src/HOL/Tools/sat_solver.ML
--- a/src/HOL/Tools/sat_solver.ML	Tue Oct 27 16:02:43 2009 +0100
+++ b/src/HOL/Tools/sat_solver.ML	Tue Oct 27 16:03:06 2009 +0100
@@ -370,13 +370,13 @@
 
   (* string * solver -> unit *)
 
-    fun add_solver (name, new_solver) =
+    fun add_solver (name, new_solver) = CRITICAL (fn () =>
       let
         val the_solvers = !solvers;
         val _ = if AList.defined (op =) the_solvers name
           then warning ("SAT solver " ^ quote name ^ " was defined before")
           else ();
-      in solvers := AList.update (op =) (name, new_solver) the_solvers end;
+      in solvers := AList.update (op =) (name, new_solver) the_solvers end);
 
 (* ------------------------------------------------------------------------- *)
 (* invoke_solver: returns the solver associated with the given 'name'        *)