agrep

slightly changed args of infer_types;
replaced parents by enclose;
renamed 2nd add_types to attach_types and fixed the
typevar-sort-constraint BUG;
various minor internal changes;

#! /bin/csh
grep "$*" {Pure/Syntax,Pure/Thy}/*ML */*ML */ex/*ML