Make the unfolding theorems collection from evalLib persistent

1 files changed, 20 insertions, 2 deletions

diff --git a/backends/hol4/primitivesBaseTacLib.sml b/backends/hol4/primitivesBaseTacLib.sml
index 3d6d9e3e..143e25ce 100644
--- a/backends/hol4/primitivesBaseTacLib.sml
+++ b/backends/hol4/primitivesBaseTacLib.sml
@@ -648,9 +648,27 @@ fun strip_all_cases_get_scrutinee (t : term) : term =
        For instance: (fst o strip_case) “if i = 0 then ... else ...”
        returns “i” while we want to get “i = 0”.
 
-       We use [dest_case] for this reason.
+       Also, [dest_case] sometimes fails.
+       
+       Ex.:
+       {[
+         val t = “result_CASE (if T then Return 0 else Fail Failure) (λy. Return ()) Fail Diverge”
+         dest_case t
+       ]}
+       TODO: file an issue
+
+       We use a custom function [get_case_scrutinee] instead of [dest_case] for this reason.
      *)
-    (strip_all_cases_get_scrutinee o (fn (_, x, _) => x) o TypeBase.dest_case) t
+    let
+      fun get_case_scrutinee t =
+        let
+          val (_, tms) = strip_comb t
+        in
+          hd tms
+        end
+    in
+    (strip_all_cases_get_scrutinee o get_case_scrutinee) t
+    end
   else t
 
 (*