bind_thm ("case_split", case_split_thm);

--- a/src/HOL/HOL_lemmas.ML	Wed Sep 29 16:45:04 1999 +0200
+++ b/src/HOL/HOL_lemmas.ML	Wed Sep 29 16:45:23 1999 +0200
@@ -422,6 +422,8 @@
   (fn [p1,p2] => [rtac (excluded_middle RS disjE) 1,
                   etac p2 1, etac p1 1]);
 
+bind_thm ("case_split", case_split_thm);
+
 fun case_tac a = res_inst_tac [("P",a)] case_split_thm;