:: deftheorem defines SCM-Compile SCM_COMP:def 12 :
for term being bin-term
for aux being Nat holds SCM-Compile (term,aux) = (SCM-Compile . term) . aux;