Merge pull request #44 from AeneasVerif/son_traits_types

Add support for traits

1 files changed, 1 insertions, 9 deletions

diff --git a/tests/hol4/hashmap/hashmap_FunsScript.sml b/tests/hol4/hashmap/hashmap_FunsScript.sml
index e3c3d2a5..682c5760 100644
--- a/tests/hol4/hashmap/hashmap_FunsScript.sml
+++ b/tests/hol4/hashmap/hashmap_FunsScript.sml
@@ -170,14 +170,6 @@ val hash_map_insert_no_resize_fwd_back_def = Define ‘
     od
 ’
 
-(** [core::num::u32::{8}::MAX] *)
-Definition core_num_u32_max_body_def:
-  core_num_u32_max_body : u32 result = Return (int_to_u32 4294967295)
-End
-Definition core_num_u32_max_c_def:
-  core_num_u32_max_c : u32 = get_return_value core_num_u32_max_body
-End
-
 val [hash_map_move_elements_from_list_loop_fwd_back_def] = DefineDiv ‘
   (** [hashmap::HashMap::{0}::move_elements_from_list]: loop 0: merged forward/backward function
       (there is a single backward function, and the forward function returns ()) *)
@@ -241,7 +233,7 @@ val hash_map_try_resize_fwd_back_def = Define ‘
       (there is a single backward function, and the forward function returns ()) *)
   hash_map_try_resize_fwd_back (self : 't hash_map_t) : 't hash_map_t result =
     do
-    max_usize <- mk_usize (u32_to_int core_num_u32_max_c);
+    max_usize <- mk_usize (u32_to_int core_u32_max);
     let capacity = vec_len self.hash_map_slots in
     do
     n1 <- usize_div max_usize (int_to_usize 2);