--- a/src/HOL/Matrix/cplex/Cplex_tools.ML Tue Sep 29 14:59:24 2009 +0200
+++ b/src/HOL/Matrix/cplex/Cplex_tools.ML Tue Sep 29 16:24:36 2009 +0200
@@ -62,7 +62,7 @@
datatype cplexSolver = SOLVER_DEFAULT | SOLVER_CPLEX | SOLVER_GLPK
-val cplexsolver = ref SOLVER_DEFAULT;
+val cplexsolver = Unsynchronized.ref SOLVER_DEFAULT;
fun get_solver () = !cplexsolver;
fun set_solver s = (cplexsolver := s);
@@ -305,8 +305,8 @@
fun load_cplexFile name =
let
val f = TextIO.openIn name
- val ignore_NL = ref true
- val rest = ref []
+ val ignore_NL = Unsynchronized.ref true
+ val rest = Unsynchronized.ref []
fun is_symbol s c = (fst c) = TOKEN_SYMBOL andalso (to_upper (snd c)) = s
@@ -612,7 +612,7 @@
fun basic_write s = TextIO.output(f, s)
- val linebuf = ref ""
+ val linebuf = Unsynchronized.ref ""
fun buf_flushline s =
(basic_write (!linebuf);
basic_write "\n";
@@ -860,7 +860,7 @@
val f = TextIO.openIn name
- val rest = ref []
+ val rest = Unsynchronized.ref []
fun readToken_helper () =
if length (!rest) > 0 then
@@ -995,7 +995,7 @@
val f = TextIO.openIn name
- val rest = ref []
+ val rest = Unsynchronized.ref []
fun readToken_helper () =
if length (!rest) > 0 then