Remove now-redundant calls to diminish_srw_ss

CakeML · Sep 14, 2022 · 5124cba · 5124cba
1 parent 6848428
commit 5124cba
Showing 1 changed file with 0 additions and 4 deletions.
diff --git a/compiler/backend/proofs/word_allocProofScript.sml b/compiler/backend/proofs/word_allocProofScript.sml
@@ -4039,8 +4039,6 @@ val is_stack_var_add= Q.prove(`
  pop_assum (qspecl_then [`na`,`4`] assume_tac)>>
  rev_full_simp_tac(srw_ss())[]));
 
-val _ = diminish_srw_ss ["MOD"]
-
 val is_alloc_var_flip = Q.prove(`
  is_alloc_var na ⇒ is_stack_var (na+2)`,
  full_simp_tac(srw_ss())[is_alloc_var_def,is_stack_var_def]>>
@@ -7185,8 +7183,6 @@ Proof
  metis_tac[ssa_cc_trans_flat_exp_conventions,FST]
 QED
 
-val _ = diminish_srw_ss ["NORMEQ"];
-
 Theorem ssa_cc_trans_full_inst_ok_less[local]:
  ∀prog ssa na c.
  every_var (λx. x < na) prog ∧