Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-02-03 00:47:35 -0800 (Thu, 03 Feb 2005)
Revision: 6577
Log message:
1. Strip type constraints at parse time after type checking.
I added the function Term_man_{ds,gen}.sweep_up_term.
I'm not sure, but this is probably not definable in
Refiner_debug, because the type
sweep_up_term : (term -> term) -> term -> term
contains a positive occurrence of the term type in an argument.
We *could* move this function out of the refiner, but it
seems a bit silly to do it. Let's see what Aleksey thinks.
2. I accidentally removed collect_opnames in Filter_cache_fun.
Added it back.
check-status now works, apart from the new theorems for reflection.
It is time to merge, at least once we decide what to do with the
sweep_up_term function.