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