src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Sat Jun 14 23:20:02 2008 +0200
+++ b/src/HOL/HOL.thy	Sat Jun 14 23:20:03 2008 +0200
@@ -731,10 +731,6 @@
 apply (erule prem1)
 done
 
-ML {*
-  fun case_split_tac P = res_inst_tac [("P", P)] @{thm case_split}
-*}
-
 (*Classical implies (-->) elimination. *)
 lemma impCE:
   assumes major: "P-->Q"