diff -r b5fbe9837aee -r 0262155d2743 src/HOL/Imperative_HOL/Heap_Monad.thy --- a/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Mar 24 18:30:17 2023 +0000 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy Fri Mar 24 18:30:17 2023 +0000 @@ -671,7 +671,7 @@ fun imp_monad_bind' (const as { sym = Code_Symbol.Constant c, dom = dom, ... }) ts = if is_bind c then case (ts, dom) of ([t1, t2], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] | ([t1, t2, t3], ty1 :: ty2 :: _) => imp_monad_bind'' [(t1, ty1), (t2, ty2)] `$ t3 - | (ts, _) => imp_monad_bind (satisfied_application 2 (const, ts)) + | (ts, _) => imp_monad_bind (saturated_application 2 (const, ts)) else IConst const `$$ map imp_monad_bind ts and imp_monad_bind (IConst const) = imp_monad_bind' const [] | imp_monad_bind (t as IVar _) = t