summaryrefslogtreecommitdiff
path: root/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig
diff options
context:
space:
mode:
Diffstat (limited to 'tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig')
-rw-r--r--tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig4
1 files changed, 2 insertions, 2 deletions
diff --git a/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig b/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig
index d4e43d9a..c19673bb 100644
--- a/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig
+++ b/tests/hol4/hashmap_main/hashmapMain_FunsTheory.sig
@@ -583,9 +583,9 @@ sig
⊢ ∀key value st.
insert_on_disk_fwd key value st =
do
- (st0,hm) <- hashmap_utils_deserialize_fwd st;
+ (st0,hm) <- utils_deserialize_fwd st;
hm0 <- hashmap_hash_map_insert_fwd_back hm key value;
- (st1,_) <- hashmap_utils_serialize_fwd hm0 st0;
+ (st1,_) <- utils_serialize_fwd hm0 st0;
Return (st1,())
od