# HG changeset patch
# User wenzelm
# Date 951251978 -3600
# Node ID 2647b7fa65088c37c0a2dbe15ed2496da8cbd4c8
# Parent  32387a2c7749347570fe7a48938264d6ab2c48c9
removed case_split thm binding;

diff -r 32387a2c7749 -r 2647b7fa6508 src/HOL/HOL_lemmas.ML
--- a/src/HOL/HOL_lemmas.ML	Tue Feb 22 21:39:01 2000 +0100
+++ b/src/HOL/HOL_lemmas.ML	Tue Feb 22 21:39:38 2000 +0100
@@ -422,8 +422,6 @@
   (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;