src/Provers/order.ML
changeset 32740 9dd0a2f83429
parent 32283 3bebc195c124
child 32768 e4a3f9c3d4f5
     1.1 --- a/src/Provers/order.ML	Tue Sep 29 14:59:24 2009 +0200
     1.2 +++ b/src/Provers/order.ML	Tue Sep 29 16:24:36 2009 +0200
     1.3 @@ -656,10 +656,10 @@
     1.4       let
     1.5    (* Ordered list of the vertices that DFS has finished with;
     1.6       most recently finished goes at the head. *)
     1.7 -  val finish : term list ref = ref nil
     1.8 +  val finish : term list Unsynchronized.ref = Unsynchronized.ref []
     1.9  
    1.10    (* List of vertices which have been visited. *)
    1.11 -  val visited : term list ref = ref nil
    1.12 +  val visited : term list Unsynchronized.ref = Unsynchronized.ref []
    1.13  
    1.14    fun been_visited v = exists (fn w => w aconv v) (!visited)
    1.15  
    1.16 @@ -715,7 +715,7 @@
    1.17  fun dfs_int_reachable g u =
    1.18   let
    1.19    (* List of vertices which have been visited. *)
    1.20 -  val visited : int list ref = ref nil
    1.21 +  val visited : int list Unsynchronized.ref = Unsynchronized.ref []
    1.22  
    1.23    fun been_visited v = exists (fn w => w = v) (!visited)
    1.24  
    1.25 @@ -755,8 +755,8 @@
    1.26  
    1.27  fun dfs eq_comp g u v =
    1.28   let
    1.29 -    val pred = ref nil;
    1.30 -    val visited = ref nil;
    1.31 +    val pred = Unsynchronized.ref [];
    1.32 +    val visited = Unsynchronized.ref [];
    1.33  
    1.34      fun been_visited v = exists (fn w => eq_comp (w, v)) (!visited)
    1.35