diff -r 22e8c115f6c9 -r 0dcafa5c9e3f src/FOL/FOL.thy
--- a/src/FOL/FOL.thy	Tue Jun 10 16:42:38 2008 +0200
+++ b/src/FOL/FOL.thy	Tue Jun 10 16:43:01 2008 +0200
@@ -66,7 +66,7 @@
     res_inst_tac [("Q",sP)] (@{thm excluded_middle} RS @{thm disjE})
 *}
 
-lemma case_split_thm:
+lemma case_split [case_names True False]:
   assumes r1: "P ==> Q"
     and r2: "~P ==> Q"
   shows Q
@@ -75,11 +75,8 @@
   apply (erule r1)
   done
 
-lemmas case_split = case_split_thm [case_names True False]
-
-(*HOL's more natural case analysis tactic*)
 ML {*
-  fun case_tac a = res_inst_tac [("P",a)] @{thm case_split_thm}
+  fun case_tac a = res_inst_tac [("P",a)] @{thm case_split}
 *}