I would say: In the dissertation Mac Lane tried to bring formal logic closer to mathematical practice. His specific device was to abbreviate certain commonly used sequences of steps into single steps. This did not turn out to be very useful and Mac Lane soon lost interest in it. The larger perspective, though, was to say that real proofs are not just any sequence of formally valid steps. He says real proofs are built around ``leading ideas.'' Mac Lane viewed his dissertation as a first step towards a ``structure theory'' of proofs that would recognize these leading ideas and use them to discover formally valid proofs. Throughout his career he believed that formal logic could help more with the actual discovery of proofs, if logicians would pay more attention to how actual proofs are used. ----- Original Message -----