src/Pure/unify.ML
changeset 32738 15bb09ca0378
parent 32032 a6a6e8031c14
child 33063 4d462963a7db
     1.1 --- a/src/Pure/unify.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/unify.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -106,7 +106,7 @@
     1.4    the occurs check must ignore the types of variables. This avoids
     1.5    that ?x::?'a is unified with f(?x::T), which may lead to a cyclic
     1.6    substitution when ?'a is instantiated with T later. *)
     1.7 -fun occurs_terms (seen: (indexname list) ref,
     1.8 +fun occurs_terms (seen: (indexname list) Unsynchronized.ref,
     1.9        env: Envir.env, v: indexname, ts: term list): bool =
    1.10    let fun occurs [] = false
    1.11    | occurs (t::ts) =  occur t  orelse  occurs ts
    1.12 @@ -160,7 +160,7 @@
    1.13  Warning: finds a rigid occurrence of ?f in ?f(t).
    1.14    Should NOT be called in this case: there is a flex-flex unifier
    1.15  *)
    1.16 -fun rigid_occurs_term (seen: (indexname list)ref, env, v: indexname, t) =
    1.17 +fun rigid_occurs_term (seen: (indexname list) Unsynchronized.ref, env, v: indexname, t) =
    1.18    let fun nonrigid t = if occurs_terms(seen,env,v,[t]) then Nonrigid
    1.19             else NoOcc
    1.20        fun occurs [] = NoOcc
    1.21 @@ -230,7 +230,7 @@
    1.22    If v occurs nonrigidly then must use full algorithm. *)
    1.23  fun assignment thy (env, rbinder, t, u) =
    1.24      let val vT as (v,T) = get_eta_var (rbinder, 0, t)
    1.25 -    in  case rigid_occurs_term (ref [], env, v, u) of
    1.26 +    in  case rigid_occurs_term (Unsynchronized.ref [], env, v, u) of
    1.27          NoOcc => let val env = unify_types thy (body_type env T,
    1.28               fastype env (rbinder,u),env)
    1.29      in Envir.update ((vT, Logic.rlist_abs (rbinder, u)), env) end
    1.30 @@ -429,7 +429,7 @@
    1.31    Attempts to update t with u, raising ASSIGN if impossible*)
    1.32  fun ff_assign thy (env, rbinder, t, u) : Envir.env =
    1.33  let val vT as (v,T) = get_eta_var(rbinder,0,t)
    1.34 -in if occurs_terms (ref [], env, v, [u]) then raise ASSIGN
    1.35 +in if occurs_terms (Unsynchronized.ref [], env, v, [u]) then raise ASSIGN
    1.36     else let val env = unify_types thy (body_type env T,
    1.37            fastype env (rbinder,u),
    1.38            env)