Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-11-12 20:48:57 -0800 (Wed, 12 Nov 2003)
Revision: 5096
Log message:

      Fixing bug 117:
      When turning a sequent into a "generic" term format, the resulting term should
      be destructed right away, not wrapped, otherwise we end up getting an
      infinite loop under Term_std.
      

Changes	Path
+7 -11	metaprl/refiner/reflib/unify_mm.ml