Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-26 01:19:06 -0800 (Thu, 26 Feb 2004)
Revision: 5415
Log message:

      Even when the domain of a substitution happens to clash with the name
      of a SO variable included in the term the substitution is being applied to,
      there is absolutely no reason for MetaPRL to complain about it. Substitutions
      just substitute for FO variables and ignore everything else (for now we still
      complain about clashes with context variables - just in case).
      

Changes	Path
+2 -4	metaprl/refiner/term_ds/term_base_ds.ml
+1 -3	metaprl/refiner/term_std/term_subst_std.ml