Introduced a generic "induct_tac" which picks up the right induction scheme
automatically. Also changed nat_ind_tac, which does no longer append a "1" to
the name of the induction variable. This caused some changes...
get_thydata accesses the second component of the data field. This component
used to be empty until set at the end of loading an ML file. Now the second
component is already set when the thy file has ben read.