Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-10 15:26:03 -0800 (Tue, 10 Jan 2006)
Revision: 8449
Log message:

      Minor adjustment fixes the problem with forward-chaining:
         use thenMT after rwhAll unfold_bsequent
      
      Apparently, the "assertion" goals produced by conditional rewrites are
      being relabeled to "main" by the forward-chainer.  I don't know why.
      
      However, there are a lot of rules in ITT with explicit [main] labels.
      So this means we'll get explicit "main" subgoals popping up randomly.
      
      BTW: what is going on with omegaT breaking all the proofs?  For some
      reason these get labeled as _my_ fault:b