clarify the addition to compile_Cexp_thm with a new no_funs constant

but evaluating Cno_funs on the result of translating the call_repl_step
dec yields F, because pattern matching - even pattern matching a literal
unit pattern - always introduces functions. so this approach is doomed.
perhaps a way to fix it is to compile the call as a special case without
going through the usual declaration machinery (and not doing any pattern
matching!), and prove special case theorems all the way up for it.