Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-24 15:08:04 -0800 (Tue, 24 Jan 2006)
Revision: 8598
Log message:

      Try to be more careful about using length{vlist{| <J> |}} as
      the canonical expression for the length of a context.
      
      Temporarily remove poplmark/naive from THEORIES_ALL until
      the proofs terminate.