src/Pure/unify.ML
changeset 20083 717b1eb434f1
parent 20020 9e7d3d06c643
child 20098 19871ee094b1
equal deleted inserted replaced
20082:b0f5981b9267 20083:717b1eb434f1
    85   | occurs (t::ts) =  occur t  orelse  occurs ts
    85   | occurs (t::ts) =  occur t  orelse  occurs ts
    86       and occur (Const _)  = false
    86       and occur (Const _)  = false
    87   | occur (Bound _)  = false
    87   | occur (Bound _)  = false
    88   | occur (Free _)  = false
    88   | occur (Free _)  = false
    89   | occur (Var (w, T))  =
    89   | occur (Var (w, T))  =
    90       if mem_ix (w, !seen) then false
    90       if member (op =) (!seen) w then false
    91       else if eq_ix(v,w) then true
    91       else if eq_ix(v,w) then true
    92         (*no need to lookup: v has no assignment*)
    92         (*no need to lookup: v has no assignment*)
    93       else (seen := w:: !seen;
    93       else (seen := w:: !seen;
    94             case Envir.lookup (env, (w, T)) of
    94             case Envir.lookup (env, (w, T)) of
    95           NONE    => false
    95           NONE    => false
   148         | occomb t = occur t
   148         | occomb t = occur t
   149       and occur (Const _)  = NoOcc
   149       and occur (Const _)  = NoOcc
   150   | occur (Bound _)  = NoOcc
   150   | occur (Bound _)  = NoOcc
   151   | occur (Free _)  = NoOcc
   151   | occur (Free _)  = NoOcc
   152   | occur (Var (w, T))  =
   152   | occur (Var (w, T))  =
   153       if mem_ix (w, !seen) then NoOcc
   153       if member (op =) (!seen) w then NoOcc
   154       else if eq_ix(v,w) then Rigid
   154       else if eq_ix(v,w) then Rigid
   155       else (seen := w:: !seen;
   155       else (seen := w:: !seen;
   156             case Envir.lookup (env, (w, T)) of
   156             case Envir.lookup (env, (w, T)) of
   157           NONE    => NoOcc
   157           NONE    => NoOcc
   158         | SOME t => occur t)
   158         | SOME t => occur t)