Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-23 15:42:28 -0800 (Wed, 23 Mar 2005)
Revision: 7020
Log message:

      Allow arbitrary non-comma terms as token _subtypes_ in term declarations.
      
      For example, the following is now legal syntax:
      
      declare sequent [Sweep[code:SweepState, kind:SweepKind{'a}]{'op : SweepOperator}] { Ignore : Prop >- 'a } : 'a
      
      where previously it would drop the "{'a}" part and insist on "kind" having
      non-existing type SweepKind{} instead of SweepKind{'a}.
      

Changes	Path
+10 -12	metaprl/filter/filter/term_grammar.ml