
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




