Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-11-03 10:38:21 -0800 (Thu, 03 Nov 2005)
Revision: 8084
Log message:

      Commented the code in Proof_boot that was removing all annotations
      from IO proofs.
      
      If I understand correctly, this code was added to clean up old proofs
      where annotations were mistakenly lying around.  That is, it was added
      for backwards compatibility.
      
      The best solution is probably just to re-export those broken proofs
      to fix the problem.  Alternately, and less satisfying, we could add
      another annotation that says "I really want to keep my annotations."
      
      We may want to add an annotation check to the subgoal/cache matcher
      so that subgoals are considered to be equal only if the annotations
      match.  This is probably good enough, or we could add an explicit
      annotation transformation rulebox before pulling in a subgoal with
      different annotations.