diff --git a/src/finite_maps/sptreeLib.sml b/src/finite_maps/sptreeLib.sml
index 251c09bfa0..d583622c65 100644
--- a/src/finite_maps/sptreeLib.sml
+++ b/src/finite_maps/sptreeLib.sml
@@ -66,6 +66,8 @@ fun add_sptree_compset compset =
       open sptreeTheory
     in
       computeLib.add_thms [
+        apsnd_cons_def,
+        combine_rle_def,
         delete_compute,
         difference_def,
         filter_v_def,
@@ -85,8 +87,12 @@ fun add_sptree_compset compset =
         mk_BS_def,
         mk_wf_def,
         size_def,
+        spt_center_def,
+        spt_centers_def,
+        spts_to_alist_def,
         toListA_def,
         toList_def,
+        toSortedAList_def,
         union_def,
         wf_def
       ] compset