working on RTac.

- ASSUMPTION now peels solved goals
  - the peeling code should be moved outward.
  - it appears that things should be relativized.
- Bug fixes to REPEAT
- Update of APPLY.
  - Now it runs a tactic as a continuation.
  - This should be generalized to support multiple goals.