Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-17 02:53:44 -0700 (Thu, 17 Jul 2003)
Revision: 4758
Log message:

      Fixed a bunch of places where dest_term was called on "special" terms.
      (Note - this should also be a big help for nested sequents support).
      

Changes  Path
+17 -19 metaprl-branches/bound_contexts/refiner/rewrite/rewrite_match_redex.ml
+189 -211 metaprl-branches/bound_contexts/refiner/term_ds/term_op_ds.ml
+27 -32 metaprl-branches/bound_contexts/refiner/term_ds/term_subst_ds.ml