--- a/src/ZF/UNITY/Monotonicity.thy	Tue Sep 27 17:54:20 2022 +0100
+++ b/src/ZF/UNITY/Monotonicity.thy	Tue Sep 27 18:02:34 2022 +0100
@@ -109,7 +109,7 @@
 
 lemma mono_munion [iff]: 
      "mono2(Mult(A), MultLe(A,r), Mult(A), MultLe(A, r), Mult(A), MultLe(A, r), munion)"
-apply (unfold mono2_def MultLe_def)
+  unfolding mono2_def MultLe_def
 apply (auto simp add: Mult_iff_multiset)
 apply (blast intro: munion_multirel_mono munion_multirel_mono1 munion_multirel_mono2 multiset_into_Mult)+
 done