diff -r 9487788a94c1 -r 9d94a6c95113 src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Fri Feb 15 17:10:09 2019 +0100
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Fri Feb 15 07:11:09 2019 +0000
@@ -962,7 +962,7 @@
           (INT h. {s. h \<le> (giv o sub i o client) s &
                             h pfixGe (ask o sub i o client) s}
                   LeadsTo {s. tokens h \<le> (tokens o rel o sub i o client) s})"
-  using image_cong_simp [cong del]
+  supply image_cong_simp [cong del]
   apply rename_client_map
   apply (simp add: Client_Progress [simplified o_def])
   done