From 1f0e5b3cb80e9334b07bf4b074c01150f4abd49d Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 22 May 2023 15:23:48 +0200
Subject: Make the unfolding theorems collection from evalLib persistent

---
 backends/hol4/divDefLib.sml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'backends/hol4/divDefLib.sml')

diff --git a/backends/hol4/divDefLib.sml b/backends/hol4/divDefLib.sml
index 1e95b6c5..c9d8806d 100644
--- a/backends/hol4/divDefLib.sml
+++ b/backends/hol4/divDefLib.sml
@@ -904,6 +904,8 @@ fun DefineDiv (def_qt : term quotation) =
        (we still do it: it doesn't cost much). *)
     val _ = app delete_binding thm_names
     val _ = map store_definition (zip thm_names def_eqs)
+    (* Also save the custom unfoldings, for evaluation (unit tests) *)
+    val _ = evalLib.add_unfold_thms thm_names
   in
     def_eqs
   end
-- 
cgit v1.2.3