diff --git a/src/symbolic/symbolic_choice.ml b/src/symbolic/symbolic_choice.ml
index 894f80820..7bc9d5fbc 100644
--- a/src/symbolic/symbolic_choice.ml
+++ b/src/symbolic/symbolic_choice.ml
@@ -38,23 +38,19 @@ module CoreImpl = struct
 
     let return_status status = Sched (Fun.const status)
 
-    let rec bind (mx : ('a, 'wls) t) (f : 'a -> ('b, 'wls) t) : _ t =
-      let rec bind_status (x : _ status) (outter_wls : 'wls) f : _ status =
+    let rec bind (mx : ('a, 'wls) t) (f : 'a -> ('b, 'wls) t) : ('b, 'wls) t =
+      let rec unfold_status (wls : 'wls) (x : ('a, 'wls) status) :
+        ('b, 'wls) status =
         match x with
-        | Now x -> run (f x) outter_wls
-        | Yield (prio, lx) ->
-          Yield (prio, Sched (fun wls -> bind_status (run lx wls) wls f))
+        | Now x -> run (f x) wls
+        | Yield (prio, lx) -> Yield (prio, bind lx f)
         | Choice (mx1, mx2) ->
-          let mx1' = bind_status mx1 outter_wls f in
-          let mx2' = bind_status mx2 outter_wls f in
+          let mx1' = unfold_status wls mx1 in
+          let mx2' = unfold_status wls mx2 in
           Choice (mx1', mx2')
         | Stop -> Stop
       in
-      Sched
-        (fun wls ->
-          match run mx wls with
-          | Yield (prio, mx) -> Yield (prio, bind mx f)
-          | x -> bind_status x wls f )
+      Sched (fun wls -> unfold_status wls (run mx wls))
 
     let ( let* ) = bind