agrep

renamed base_on into mk_base and moved it to the beginning of the generated
.thy.ML file to make sure that all base theories are present when ML executes
the rest of this file

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