--- a/src/HOL/HOL_lemmas.ML Tue Sep 21 17:26:50 1999 +0200
+++ b/src/HOL/HOL_lemmas.ML Tue Sep 21 17:28:02 1999 +0200
@@ -412,7 +412,6 @@
etac p2 1, etac p1 1]);
fun case_tac a = res_inst_tac [("P",a)] case_split_thm;
-bind_thm ("case", case_split_thm);
(** Standard abbreviations **)