# HG changeset patch
# User berghofe
# Date 1067424626 -3600
# Node ID 399a3290936c3ee656affb52c6f2e8bcd26a1c8a
# Parent  cb32eb89bddd68acd03c00b62133e2c68d5c9446
Tuned proof of choice_eq.

diff -r cb32eb89bddd -r 399a3290936c src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Wed Oct 29 01:17:06 2003 +0100
+++ b/src/HOL/HOL.thy	Wed Oct 29 11:50:26 2003 +0100
@@ -540,7 +540,6 @@
   apply (rule allI)
   apply (rule ex1I)
   apply (erule spec)
-  apply (rule ccontr)
   apply (erule_tac x = "%z. if z = x then y else f z" in allE)
   apply (erule impE)
   apply (rule allI)