# HG changeset patch
# User wenzelm
# Date 937927682 -7200
# Node ID 19c3be2d285cae15ec1c05695fd01ec23f6a4156
# Parent  1d2c099e98f78fa9c8f166ef63205f073cc86a7a
removed "case" thm;

diff -r 1d2c099e98f7 -r 19c3be2d285c src/HOL/HOL_lemmas.ML
--- 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 **)