Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2001-11-03 12:12:33 -0800 (Sat, 03 Nov 2001)
Revision: 3437
Log message:

      When we replace a goal of a RuleBox, it seems a better idea to use
      Unjustified as a new rule_extract instead of just Goal - this way we
      preserve the original leaf information and only (re)expansion of a
      RuleBox may alter its list of leaves.
      
      Before this change leaf mismatches were producing "nasty" side-effects
      when people were attempting to work inside non-expanded proofs.
      

Changes	Path
+17 -13	metaprl/filter/boot/proof_boot.ml