Fix another def_compute

CakeML · Aug 4, 2019 · 91e01be · 91e01be
1 parent e2643a9
commit 91e01be
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/compiler/backend/ag32/proofs/ag32_memoryProofScript.sml b/compiler/backend/ag32/proofs/ag32_memoryProofScript.sml
@@ -896,7 +896,7 @@ val bare_asm_conv =
      combinLib.add_combin_compset],
     computeLib.Defs [
       UPDATE_def,
-      asmSemTheory.write_mem_word_def_compute],
+      asmSemTheory.write_mem_word_compute],
     computeLib.Tys [``:'a asmSem$asm_state``]])
 
 val asm_conv =