function unify( a, b :tree; var newenv :Env; oldenv :Env) :boolean;
   var e2 :Env; v :tree;
begin {unify}
   newenv := oldenv;
   if (a = nil) or (b=nil) then unify := a=b
   
   else { a<>nil and b<>nil } if a^.tag = b^.tag then
         case a^.tag { = b^.tag } of
         variable: if bound(a, v, oldenv) then
                      unify := unify(v, b, newenv, oldenv)
                   else if bound(b, v, oldenv) then
                      unify := unify(a, v, newenv, oldenv)
                                                                 {both unbound}
                   else if (a^.vid=b^.vid) and (a^.index=b^.index) then
                      unify := true
                   else {2 different, unbound vars}
                   begin newenv := bind(a, b, oldenv); unify := true
                   end;
         
         constant: unify := a^.cid = b^.cid;                        { m  :  n }
         
         intcon:   unify := a^.n = b^.n;                            { x  :  y }
         
         func, predicate:                                 { a(...)  :  b(...) }
                   if a^.id = b^.id then
                      unify := unify(a^.params, b^.params, newenv, oldenv)
                   else unify := false;
                                                         { ahd.atl  : bhd.btl }
         list:     if unify(a^.hd, b^.hd, e2, oldenv) then
                      unify := unify(a^.tl, b^.tl, newenv, e2)
                   else unify := false
         end {case}
      
   else { a^.tag <> b^.tag } if a^.tag = variable then         { X  :  f(...) }
      if bound(a, v, oldenv) then
         unify := unify(v, b, newenv, oldenv)
      else
      begin newenv := bind(a, b, oldenv); unify := true
      end
      
   else if b^.tag = variable then                              { f(...)  :  X }
      unify := unify(b, a, newenv, oldenv)
      
   else unify := false
end  {unify};

{\fB Unification Algorithm. \fP}
{Do not remove: Main.p, env*P, execute.P, unify.P, rename.P, prove.P, lex*P, }
{ syntax*P, tree.P are released under Gnu `copyleft' General Public Licence  }
{ - L. Allison, CSSE, Monash Uni., .au, 7/2003.                              }