--- a/src/ZF/upair.thy Sun May 20 16:25:27 2018 +0200
+++ b/src/ZF/upair.thy Sun May 20 18:45:18 2018 +0200
@@ -230,10 +230,10 @@
**)
lemmas split_if_eq1 = split_if [of "%x. x = b"] for b
-lemmas split_if_eq2 = split_if [of "%x. a = x"] for x
+lemmas split_if_eq2 = split_if [of "%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 x
+lemmas split_if_mem2 = split_if [of "%x. a \<in> x"] for a
lemmas split_ifs = split_if_eq1 split_if_eq2 split_if_mem1 split_if_mem2