Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 1998-07-07 21:55:43 -0700 (Tue, 07 Jul 1998)
Revision: 2313
Log message:

      Added apply_fun_higher : (term -> term * 'a) -> term -> term * 'a list
      The 'a list returned lists all successful applications of the function
      "left to right".
      When the function raises RefineError _ everywhere inside some subterm,
      the sharing is preserved.
      

Changes	Path
+4 -0	metaprl/refiner/refsig/term_addr_sig.ml
+20 -0	metaprl/refiner/term_gen/term_addr_gen.mlp