diff -r 7a98dbf3e579 -r cee6d5aee7c8 src/HOL/Set.ML
--- a/src/HOL/Set.ML	Wed Jun 28 10:40:06 2000 +0200
+++ b/src/HOL/Set.ML	Wed Jun 28 10:41:16 2000 +0200
@@ -19,8 +19,6 @@
 by (Asm_full_simp_tac 1);
 qed "CollectD";
 
-bind_thm ("CollectE", make_elim CollectD);
-
 val [prem] = Goal "[| !!x. (x:A) = (x:B) |] ==> A = B";
 by (rtac (prem RS ext RS arg_cong RS box_equals) 1);
 by (rtac Collect_mem_eq 1);