Fix a mistake

CakeML · Nov 9, 2021 · 13eb6f5 · 13eb6f5
1 parent c752e23
commit 13eb6f5
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/examples/lpr_checker/array/compilation/proofs/lpr_arrayRamseyProofScript.sml b/examples/lpr_checker/array/compilation/proofs/lpr_arrayRamseyProofScript.sml
@@ -121,7 +121,7 @@ Proof
       metis_tac[STD_streams_stderr,add_stdo_nil]>>
     match_mp_tac ramsey_eq>>simp[not_is_ramsey_4_17]>>
     match_mp_tac ramsey_lpr_correct>>
-    match_mp_tac (GEN_ALL check_lpr_unsat_list_sound)>>
+    match_mp_tac (GEN_ALL lpr_arrayProgTheory.check_lpr_unsat_list_sound)>>
     fs[enc_def]>>
     asm_exists_tac>>simp[]>>
     CONJ_TAC >- (