Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-11-04 09:27:20 -0800 (Fri, 04 Nov 2005)
Revision: 8095
Log message:

      Relaxed a bit the test for "may be patterns". If all occurrences of a second
      variable in the redex are "pattern-like" occurrences inside another second
      order variable (which means that in the actual match in may not occur at all
      if that other SO variable does not depend on its argument), the rewriter used
      to complain. I've changed it so that if that SO variable does not occur in the
      contractum, then rewriter accepts such rewrite.
      
      Example:
      
      interactive tunionHyp {| nth_hyp |} 'H :
         sequent { <H>; x: 'B['a]; <J['x]> >- 'x in Union x:'A. 'B['x]  }
         
      Here the rewriter used to complain that 'a does not have a pattern and needs
      to be passed in as an argument, which is clearly unnecessary in this case.