Make a proof more robust

I suggest avoiding use of EVAL_TAC if several lines of
tactic follow the call to EVAL_TAC.

compiler/backend/proofs/stack_to_labProofScript.sml

@@ -1793,11 +1793,12 @@ Proof
     full_simp_tac(srw_ss())[call_args_def] >> var_eq_tac >>
     imp_res_tac find_code_lookup >>
     `dest_to_loc (s.regs \\ t1.link_reg) dest = dest_to_loc' t1.regs dest` by (
-      EVAL_TAC >>
-      CASE_TAC >> full_simp_tac(srw_ss())[] >>
+      fs [dest_to_loc_def,dest_to_loc'_def] >>
+      TOP_CASE_TAC >>
+      fs [find_code_def,option_case_eq,CaseEq"word_loc",num_case_eq] >>
+      rveq >> fs [DOMSUB_FAPPLY_THM,FLOOKUP_DEF] >>
       qhdtm_x_assum`state_rel`mp_tac >>
-      simp[DOMSUB_FAPPLY_THM] >>
-      simp[state_rel_def,FLOOKUP_DEF] ) >>
+      simp[state_rel_def,FLOOKUP_DEF]) >>
     full_simp_tac(srw_ss())[] >>
     first_assum(fn th => first_assum(
       tryfind (strip_assume_tac o C MATCH_MP th) o CONJUNCTS o CONV_RULE (REWR_CONV state_rel_def))) >>