From d2825f37136128f5ac92127020a4b4a58bce3636 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 22 Feb 2018 17:03:42 +0000
Subject: Some Lem/OCaml compatibility fixes

---
 src/gen_lib/sail_values.lem | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'src/gen_lib/sail_values.lem')

diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index 33caac37..b981bb91 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -379,11 +379,13 @@ end
 (* just_list takes a list of maybes and returns Just xs if all elements have
    a value, and Nothing if one of the elements is Nothing. *)
 val just_list : forall 'a. list (maybe 'a) -> maybe (list 'a)
-let rec just_list [] = Just []
-and just_list (x :: xs) =
-  match (x, just_list xs) with
-    | (Just x, Just xs) -> Just (x :: xs)
-    | (_, _) -> Nothing
+let rec just_list l = match l with
+  | [] -> Just []
+  | (x :: xs) ->
+    match (x, just_list xs) with
+      | (Just x, Just xs) -> Just (x :: xs)
+      | (_, _) -> Nothing
+    end
   end
 declare {isabelle} termination_argument just_list = automatic
 
-- 
cgit v1.2.3