Lem/OCaml compatibility fixes

2 files changed, 10 insertions, 4 deletions

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index bca09aa1..9642c714 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -20,10 +20,13 @@ let iter f xs = iteri (fun _ x -> f x) xs
 
 val foreachM : forall 'a 'rv 'vars 'e.
   list 'a -> 'vars -> ('a -> 'vars -> monad 'rv 'vars 'e) -> monad 'rv 'vars 'e
-let rec foreachM [] vars _ = return vars
-and foreachM (x :: xs) vars body =
+let rec foreachM l vars body =
+match l with
+| [] -> return vars
+| (x :: xs) ->
   body x vars >>= fun vars ->
   foreachM xs vars body
+end
 
 declare {isabelle} termination_argument foreachM = automatic
 
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index ead63d62..4d67cbfc 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -752,8 +752,11 @@ let internal_mem_value bytes =
 
 val foreach : forall 'a 'vars.
   (list 'a) -> 'vars -> ('a -> 'vars -> 'vars) -> 'vars
-let rec foreach [] vars _ = vars
-and foreach (x :: xs) vars body = foreach xs (body x vars) body
+let rec foreach l vars body =
+match l with
+| [] -> vars
+| (x :: xs) -> foreach xs (body x vars) body
+end
 
 declare {isabelle} termination_argument foreach = automatic