From 395c80b348616fe6e0af7e6b5af491c3bb138f73 Mon Sep 17 00:00:00 2001 From: Michael Norrish Date: Tue, 10 Jan 2023 15:30:43 +1100 Subject: [PATCH] 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. --- translator/monadic/ml_monadStoreLib.sml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/translator/monadic/ml_monadStoreLib.sml b/translator/monadic/ml_monadStoreLib.sml index 11b47b25e6..cac01d393e 100644 --- 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