From ce8f5c8f67e41a74bfdf8f6d664ff4e45e9de850 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 7 Sep 2023 16:06:14 +0200
Subject: Regenerate the test files and fix a proof

---
 tests/hol4/hashmap/hashmap_PropertiesScript.sml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tests/hol4/hashmap/hashmap_PropertiesScript.sml')

diff --git a/tests/hol4/hashmap/hashmap_PropertiesScript.sml b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
index 7259f2f5..8bc12fa5 100644
--- a/tests/hol4/hashmap/hashmap_PropertiesScript.sml
+++ b/tests/hol4/hashmap/hashmap_PropertiesScript.sml
@@ -1296,7 +1296,7 @@ Proof
   rw [hash_map_try_resize_fwd_back_def] >>
   (* “_ <-- mk_usize (u32_to_int core_num_u32_max_c)” *)
   assume_tac usize_u32_bounds >>
-  fs [core_num_u32_max_c_def, core_num_u32_max_body_def, get_return_value_def, u32_max_def] >>
+  fs [core_u32_max_def, u32_max_def] >>
   massage >> fs [mk_usize_def, u32_max_def] >>
   (* / 2 *)
   progress >>
-- 
cgit v1.2.3