3 files changed, 21 insertions, 17 deletions
diff --git a/src/gen_lib/prompt_monad.lem b/src/gen_lib/prompt_monad.lem
index ff5e3726..38f79868 100644
--- a/src/gen_lib/prompt_monad.lem
+++ b/src/gen_lib/prompt_monad.lem
@@ -125,7 +125,7 @@ let write_mem_val v = match bytes_of_bits v with
   | Just v ->
      let k successful = (return successful) in
      Write_memv (List.reverse v) k
-  | Nothing -> fail "write_mem_val"
+  | Nothing -> Fail "write_mem_val"
 end
 
 val read_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> monad 'rv 'a 'e
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
 
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 4675428e..fba8d9b7 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -9,17 +9,19 @@ open import {isabelle} `State_monad_extras`
 (* State monad wrapper around prompt monad *)
 
 val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
-let rec liftState _ (Done a)          = returnS a
-and liftState ra (Read_mem rk a sz k) = bindS (read_memS rk a sz)     (fun v -> liftState ra (k v))
-and liftState ra (Write_memv descr k) = bindS (write_mem_valS descr)  (fun v -> liftState ra (k v))
-and liftState ra (Read_reg descr k)   = bindS (read_regvalS ra descr) (fun v -> liftState ra (k v))
-and liftState ra (Excl_res k)         = bindS (excl_resultS ())       (fun v -> liftState ra (k v))
-and liftState ra (Write_ea wk a sz k) = seqS (write_mem_eaS wk a sz)  (liftState ra k)
-and liftState ra (Write_reg r v k)    = seqS (write_regvalS ra r v)   (liftState ra k)
-and liftState ra (Barrier _ k)        = liftState ra k
-and liftState _  (Fail descr)         = failS descr
-and liftState _  (Error descr)        = failS descr
-and liftState _  (Exception e)        = throwS e
+let rec liftState ra s = match s with
+  | (Done a)             -> returnS a
+  | (Read_mem rk a sz k) -> bindS (read_memS rk a sz)     (fun v -> liftState ra (k v))
+  | (Write_memv descr k) -> bindS (write_mem_valS descr)  (fun v -> liftState ra (k v))
+  | (Read_reg descr k)   -> bindS (read_regvalS ra descr) (fun v -> liftState ra (k v))
+  | (Excl_res k)         -> bindS (excl_resultS ())       (fun v -> liftState ra (k v))
+  | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz)  (liftState ra k)
+  | (Write_reg r v k)    -> seqS (write_regvalS ra r v)   (liftState ra k)
+  | (Barrier _ k)        -> liftState ra k
+  | (Fail descr)         -> failS descr
+  | (Error descr)        -> failS descr
+  | (Exception e)        -> throwS e
+end
 
 
 (* TODO