src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML
changeset 32740 9dd0a2f83429
parent 31971 8c1b845ed105
     1.1 --- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -136,7 +136,7 @@
     1.4  
     1.5  fun cplexProg c A b =
     1.6      let
     1.7 -        val ytable = ref Inttab.empty
     1.8 +        val ytable = Unsynchronized.ref Inttab.empty
     1.9          fun indexof s =
    1.10              if String.size s = 0 then raise (No_name s)
    1.11              else case Int.fromString (String.extract(s, 1, NONE)) of
    1.12 @@ -145,7 +145,7 @@
    1.13          fun nameof i =
    1.14              let
    1.15                  val s = "x"^(Int.toString i)
    1.16 -                val _ = change ytable (Inttab.update (i, s))
    1.17 +                val _ = Unsynchronized.change ytable (Inttab.update (i, s))
    1.18              in
    1.19                  s
    1.20              end
    1.21 @@ -242,7 +242,7 @@
    1.22  
    1.23  fun cut_vector size v =
    1.24    let
    1.25 -    val count = ref 0;
    1.26 +    val count = Unsynchronized.ref 0;
    1.27      fun app (i, s) =  if (!count < size) then
    1.28          (count := !count +1 ; Inttab.update (i, s))
    1.29        else I