function rename(t :tree; index :integer) :tree;
   var r :tree;

   function copynode :tree;
      var c :tree;
   begin c:=newnode(t^.tag); c^:=t^; copynode:=c
   end;

begin{rename}
   if t = nil then r := nil
   else
      case t^.tag of
         variable:begin r:=copynode; r^.index:=index end;
         constant:r := t;
         intcon:  r := t;
         predicate, func:
                  begin r := copynode; r^.params := rename(t^.params, index)
                  end;
         negate:  begin r := copynode; r^.l := rename(t^.l, index) end;
         rule:    begin r := copynode;
                        r^.lhs := rename(t^.lhs, index);
                        r^.rhs := rename(t^.rhs, index)
                  end;
         list:    begin r := copynode;
                        r^.hd := rename(t^.hd, index);
                        r^.tl := rename(t^.tl, index)
                  end;
      end{case};
   rename := r
end{rename};

{\fB Rename Variables in a Tree. \fP}