Fix proof broken by HOL's removal of relationTheory.RTC_DEF

CakeML · Jul 24, 2019 · 771865c · 771865c
1 parent 7fd7091
commit 771865c
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/compiler/backend/proofs/data_to_word_memoryProofScript.sml b/compiler/backend/proofs/data_to_word_memoryProofScript.sml
@@ -6950,7 +6950,7 @@ Proof
       bc_ref_inv c i2 refs (f,heap,be)` by
    (rpt strip_tac \\ first_x_assum match_mp_tac
     \\ fs [reachable_refs_def]
-    \\ metis_tac [get_refs_def,MEM,RTC_DEF])
+    \\ metis_tac [get_refs_def,MEM,RTC_CASES1])
   \\ fs [bc_ref_inv_def,FLOOKUP_DEF] \\ rfs [SUBSET_DEF]
   \\ NTAC 2 (pop_assum mp_tac) \\ fs []
   \\ rpt strip_tac