# HG changeset patch
# User wenzelm
# Date 1350566108 -7200
# Node ID b76937179ff5e97929f021b1f2bc8bbde28d34c6
# Parent  c6307ee2665df5a21eb157cf6b9e0ce58fca9519
fixed proof (cf. a81f95693c68);

diff -r c6307ee2665d -r b76937179ff5 src/HOL/Cardinals/Wellorder_Embedding_Base.thy
--- a/src/HOL/Cardinals/Wellorder_Embedding_Base.thy	Thu Oct 18 14:15:46 2012 +0200
+++ b/src/HOL/Cardinals/Wellorder_Embedding_Base.thy	Thu Oct 18 15:15:08 2012 +0200
@@ -722,8 +722,8 @@
                           (snd o h1) y = (snd o h2) y" by auto
     hence "(fst o h1)`(rel.underS r x) = (fst o h2)`(rel.underS r x) \<and>
            (snd o h1)`(rel.underS r x) = (snd o h2)`(rel.underS r x)"
-    by (auto simp add: image_def)
-    thus "H h1 x = H h2 x" by (simp add: H_def)
+      by (auto simp add: image_def)
+    thus "H h1 x = H h2 x" by (simp add: H_def del: not_False_in_image_Ball)
   qed
   (* More constant definitions:  *)
   obtain h::"'a \<Rightarrow> 'a' * bool" and f::"'a \<Rightarrow> 'a'" and g::"'a \<Rightarrow> bool"