Fix breakage caused by HOL-Theorem-Prover/HOL@29ebd7ceac5df

The API for Redblackmap has become richer and now includes a filter entry-point; this can mask List.filter, as happened here.
CakeML · Jan 10, 2023 · 395c80b · 395c80b
1 parent d7c520f
commit 395c80b
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/translator/monadic/ml_monadStoreLib.sml b/translator/monadic/ml_monadStoreLib.sml
@@ -14,6 +14,8 @@ open ml_monadBaseTheory ml_monad_translatorBaseTheory ml_monad_translatorTheory
 open Redblackmap AC_Sort Satisfy
 open ml_translatorLib
 
+val filter = List.filter (* reverse masking by Redblackmap's filter *)
+
 (* COPY/PASTE from other manual eval_rel proofs *)
 fun derive_eval_thm for_eval v_name e = let
   val env = get_ml_prog_state () |> get_env