Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-08-13 11:47:39 -0700 (Wed, 13 Aug 2003)
Revision: 4836
Log message:

      Updated the sequent code in Unify_mm.  The idea is to add a "compatibility
      layer" that converts sequents to the old format for use during unification,
      and these sequents have to be converted back to normal form when the
      unification is done.
      
      To do this, we just redefine dest_term and make_term to do the right thing.
      

Changes	Path
+179 -135	metaprl/refiner/reflib/unify_mm.ml
+5 -0	metaprl/refiner/reflib/unify_mm.mli
+14 -0	metaprl/support/shell/shell.ml
+4 -0	metaprl/support/shell/shell.mli