Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-02-23 19:01:26 -0800 (Thu, 23 Feb 2006)
Revision: 8781
Log message:

      Copy display forms to reflected theories.  The display forms
      clearly need some work, but they will do for now.
      
         - quote the redex
         - wrap the contractum in reflect_df{'def} for mk_term,
           and reflect_df{'d; 'def} for mk_bterm.