Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-04-16 16:01:41 -0700 (Fri, 16 Apr 2004)
Revision: 5662
Log message:
This implements bug 188:
Now in prim rules syntax the "= term" extract specification is optional.
By default (e.g. if the extract specification is omited), the extract
is taken to be "default_extract{}". The system will still complain if the
default_extract opname is not declared, making the extracts truly optional
only in theories that declare such an opname.
For now, the only theory that uses this is the fir one (which I used to test
the implemention).