improve inst_labels_fn_intro

in particular, trade the expensive IS_PTREE and PERM (TRAVERSE)
hypotheses for a code_labels_ok hypothesis - which should hopefully come
for free because the code comes out of the compiler.

have not updated labels_computeLib.sml to make use of this better
theorem.