diff --git a/src/Ouroboros-Mini_Protocols-Chain_Sync.thy b/src/Ouroboros-Mini_Protocols-Chain_Sync.thy
index 336e7c1..b355811 100644
--- a/src/Ouroboros-Mini_Protocols-Chain_Sync.thy
+++ b/src/Ouroboros-Mini_Protocols-Chain_Sync.thy
@@ -79,8 +79,8 @@ datatype phase =
   is_intersection_finding: IntersectionFinding |
   is_chain_update: ChainUpdate
 
-definition roll_back_to :: "'i list \<Rightarrow> 'p \<Rightarrow> ('i \<Rightarrow> 'p) \<Rightarrow> 'i list" where
-  [simp]: "roll_back_to \<C> p \<psi> = (THE \<C>\<^sub>1. \<exists>\<C>\<^sub>2. \<C> = \<C>\<^sub>1 @ \<C>\<^sub>2 \<and> \<psi> (last \<C>\<^sub>1) = p)"
+definition roll_back_to :: "('i \<Rightarrow> 'p) \<Rightarrow> 'i list \<Rightarrow> 'p \<Rightarrow> 'i list" where
+  [simp]: "roll_back_to \<psi> \<C> p = (THE \<C>\<^sub>1. \<exists>\<C>\<^sub>2. \<C> = \<C>\<^sub>1 @ \<C>\<^sub>2 \<and> \<psi> (last \<C>\<^sub>1) = p)"
 
 corec client_program where
   "client_program ph \<kappa> \<psi> \<C> = (
@@ -100,7 +100,7 @@ corec client_program where
           Cont (RollForward i) \<Rightarrow>
             client_program ph \<kappa> \<psi> (\<C> @ [i]) |
           Cont (RollBackward p) \<Rightarrow>
-            client_program ph \<kappa> \<psi> (roll_back_to \<C> p \<psi>) |
+            client_program ph \<kappa> \<psi> (roll_back_to \<psi> \<C> p) |
           Cont AwaitReply \<Rightarrow> \<comment> \<open>client is up to date\<close>
             \<up> Done;
             \<bottom>