Reasoning behind design of annotateWithSystems and execProofMethod

[felixlinker]

The function execProofMethod returns Proof () and only annotates the proof steps with the methods solved, but does execute the proof method itself. annotateWithSystems then takes these annotations and saves the resulting system in the proof tree. This causes another call to execProofMethod (here), and I presume, that Haskell is not lazy enough to figure out that these two calls have the same result. See this line.

Does anybody know the reasoning behind this design? Why not let execProofMethod return Proof (Maybe System) immediately?