Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-04-04 23:45:28 -0700 (Mon, 04 Apr 2005)
Revision: 7134
Log message:

      With TERMS=std, we were getting an "illegal subterm Perv!concl{...}" error
      message (because of the Term_man_gen encoding for sequents using the internal
      operators for encoding sequents). I added a hack that skips the "internal"
      sequent subterms when iterating/mapping over terms (those should not be
      getting exposed anyway).
      

Changes	Path
+13 -4	metaprl/refiner/term_std/term_op_std.ml