--- a/src/ZF/upair.thy Tue Sep 27 17:03:23 2022 +0100
+++ b/src/ZF/upair.thy Tue Sep 27 17:46:52 2022 +0100
@@ -229,11 +229,11 @@
(** Rewrite rules for boolean case-splitting: faster than split_if [split]
**)
-lemmas split_if_eq1 = split_if [of "%x. x = b"] for b
-lemmas split_if_eq2 = split_if [of "%x. a = x"] for a
+lemmas split_if_eq1 = split_if [of "\<lambda>x. x = b"] for b
+lemmas split_if_eq2 = split_if [of "\<lambda>x. a = x"] for a
-lemmas split_if_mem1 = split_if [of "%x. x \<in> b"] for b
-lemmas split_if_mem2 = split_if [of "%x. a \<in> x"] for a
+lemmas split_if_mem1 = split_if [of "\<lambda>x. x \<in> b"] for b
+lemmas split_if_mem2 = split_if [of "\<lambda>x. a \<in> x"] for a
lemmas split_ifs = split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2