Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
functions from sign.ML to thm.ML or drule.ML. This allows the "prop" field
of a theorem to be regarded as a cterm -- avoids expensive calls to
cterm_of.

 #! /bin/csh

 grep "$*" {Pure/Syntax,Pure/Thy}/*ML */*ML */ex/*ML