Well, fwiw here's another attempt at simp_assuming ...
simp_assuming (e, [fcts])::=buildq ([e, fcts],
unwind_protect ((apply (supcontext, ?gensym ("cntxt")]),
apply (assume, fcts),
expand (e, 0, 0)),
killcontext (context)));
(killcontext(context) kills the current context whatever it is,
so it isn't necessary to remember the gensym.)
Does that work any better?
best
Robert Dodier