Fix for change in HOL

CakeML · Dec 19, 2023 · 6dbde16 · 6dbde16
1 parent 4ce61c3
commit 6dbde16
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/pancake/proofs/loop_removeProofScript.sml b/pancake/proofs/loop_removeProofScript.sml
@@ -173,6 +173,7 @@ Proof
        by fs [EXTENSION,domain_lookup,MEM_MAP,EXISTS_PROD]
   \\ fs [spt_eq_thm,wf_inter,wf_fromAList,lookup_fromAList,lookup_inter_alt]
   \\ pop_assum kall_tac \\ pop_assum kall_tac
+  \\ rewrite_tac [GSYM sptreeTheory.LENGTH_toAList]
   \\ rename [‘MAP FST xs’]
   \\ Induct_on ‘xs’ \\ fs [get_vars_def,FORALL_PROD]
   \\ rw [] \\ fs [domain_lookup] \\ rw [] \\ fs []