POP_ASSUM : thm_tactic -> tactic
POP_ASSUM f ({A1;...;An} ?- t) = f (... |- A1) ({A2;...;An} ?- t)
DISCH_TAC THEN POP_ASSUM (fun th -> SUBST1_TAC (SYM th))
DISCH_THEN (SUBST1_TAC o SYM)
# g `!f x. 0 = x ==> f(x * f(x)) = f(x)`;;
# e(REPEAT STRIP_TAC);; val it : goalstack = 1 subgoal (1 total) 0 [`0 = x`] `f (x * f x) = f x`
# e(POP_ASSUM(SUBST1_TAC o SYM) THEN REWRITE_TAC[MULT_CLAUSES]);;
# e(REWRITE_TAC[MULT_CLAUSES; SYM(ASSUME `0 = x`)]);;
# e(REPEAT GEN_TAC THEN DISCH_THEN(SUBST1_TAC o SYM) THEN REWRITE_TAC[MULT_CLAUSES]);;