Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-23 20:27:09 -0800 (Thu, 23 Feb 2006)
Revision: 8783
Log message:

      Working on reflecting more stuff.
      
      It isn't clear whether grammars should be included in a reflected theory.
      In any case, we can postpone for now.
      
      However, at least the original theory should be able to define a grammar.
      Then we get weird stuff in the original theory like:
      
         declare tok_foo : Terminal
         define iform succ{'x} <--> 'x +@ 1
      
      From the point of view of the reflected logic, we want to ignore this
      junk.
      
      I think the only thing that can't be easily filtered out is the "declare
      tok_foo : Terminal".  I don't like filtering based on the semantic info--
      I prefer filtering based on syntactic info...
      
      Would we be willing to define a new shapeclass, and define tokens in
      the following way (rather than the way we do now)?
      
         declare token tok_foo