# HG changeset patch
# User nipkow
# Date 1527172704 -7200
# Node ID d231238bd977ca830aa52079200b7ce44c2acdf2
# Parent  035c78bb0a6675e8b5e9c5b42daa6410b353c1a0
tuned

diff -r 035c78bb0a66 -r d231238bd977 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Thu May 24 14:42:47 2018 +0200
+++ b/src/HOL/Wellfounded.thy	Thu May 24 16:38:24 2018 +0200
@@ -258,18 +258,18 @@
     and inj: "\<And> a a'. a \<in> Domain r \<Longrightarrow> a' \<in> Range r \<Longrightarrow> f a = f a' \<Longrightarrow> a = a'"
   shows "wf (map_prod f f ` r)"
 proof (unfold wf_eq_minimal, clarify)
-  fix Q::"'b set" and b::"'b"
-  assume b: "b \<in> Q"
-  define Q' where "Q' \<equiv> f -` Q \<inter> Domain r"
-  show "\<exists>z\<in>Q. \<forall>y. (y, z) \<in> map_prod f f ` r \<longrightarrow> y \<notin> Q"
-  proof (cases "Q' = {}")
+  fix B :: "'b set" and b::"'b"
+  assume "b \<in> B"
+  define A where "A = f -` B \<inter> Domain r"
+  show "\<exists>z\<in>B. \<forall>y. (y, z) \<in> map_prod f f ` r \<longrightarrow> y \<notin> B"
+  proof (cases "A = {}")
     case False
-    then obtain b0 where "b0\<in>Q'" and "\<forall>b. (b, b0) \<in> r \<longrightarrow> b \<notin> Q'"
+    then obtain a0 where "a0 \<in> A" and "\<forall>a. (a, a0) \<in> r \<longrightarrow> a \<notin> A"
       using wfE_min[OF wf_r] by auto
     thus ?thesis 
-      using inj unfolding Q'_def   
-      by (intro bexI[of _ "f b0"]) auto
-  qed(insert b, unfold Q'_def, auto) 
+      using inj unfolding A_def
+      by (intro bexI[of _ "f a0"]) auto
+  qed (insert \<open>b \<in> B\<close>, unfold A_def, auto) 
 qed
 
 lemma wf_map_prod_image: "wf r \<Longrightarrow> inj f \<Longrightarrow> wf (map_prod f f ` r)"