bind_thm "case";

--- 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 **)