src/Provers/order.ML
changeset 32740 9dd0a2f83429
parent 32283 3bebc195c124
child 32768 e4a3f9c3d4f5
--- a/src/Provers/order.ML	Tue Sep 29 14:59:24 2009 +0200
+++ b/src/Provers/order.ML	Tue Sep 29 16:24:36 2009 +0200
@@ -656,10 +656,10 @@
      let
   (* Ordered list of the vertices that DFS has finished with;
      most recently finished goes at the head. *)
-  val finish : term list ref = ref nil
+  val finish : term list Unsynchronized.ref = Unsynchronized.ref []
 
   (* List of vertices which have been visited. *)
-  val visited : term list ref = ref nil
+  val visited : term list Unsynchronized.ref = Unsynchronized.ref []
 
   fun been_visited v = exists (fn w => w aconv v) (!visited)
 
@@ -715,7 +715,7 @@
 fun dfs_int_reachable g u =
  let
   (* List of vertices which have been visited. *)
-  val visited : int list ref = ref nil
+  val visited : int list Unsynchronized.ref = Unsynchronized.ref []
 
   fun been_visited v = exists (fn w => w = v) (!visited)
 
@@ -755,8 +755,8 @@
 
 fun dfs eq_comp g u v =
  let
-    val pred = ref nil;
-    val visited = ref nil;
+    val pred = Unsynchronized.ref [];
+    val visited = Unsynchronized.ref [];
 
     fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)