agrep

ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
ex/prop-log/hyps_thms_if: split up the fast_tac call for more speed
called expandshort

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