--- a/src/HOL/HOL_lemmas.ML Wed Sep 01 21:24:50 1999 +0200
+++ b/src/HOL/HOL_lemmas.ML Wed Sep 01 21:25:17 1999 +0200
@@ -412,6 +412,7 @@
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 **)