Changes by: Jason J. Hickey (jyh at cs.caltech.edu)
Date: 2008-02-03 14:40:37 -0800 (Sun, 03 Feb 2008)
Revision: 12717
Log message:

      Some minor changes to fight bitrot.
     
     There is something wrong with nthHypT.  If I write a rule like this,
     it will not apply with nthHypT (failWithT: no match).
     
        prim axiom {| nth_hyp |} 'H : <:xrule<
           <H>; A; <J> >- A
        >>
     
     If it add a binder, it works.
     
        prim axiom {| nth_hyp |} 'H : <:xrule<
           <H>; x: A; <J[x]> >- A
        >>
     
     Same happens even if I use traditional syntax.