src/HOL/Hoare/Hoare.ML

 (**Simp_tacs**)
 
 val before_set2pred_simp_tac =
   (simp_tac (HOL_basic_ss addsimps [Collect_conj_eq RS sym,Compl_Collect]));
 
-val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split]));
+val split_simp_tac = (simp_tac (HOL_basic_ss addsimps [split_conv]));
 
 (*****************************************************************************)
 (** set2pred transforms sets inclusion into predicates implication,         **)
 (** maintaining the original variable names.                                **)
 (** Ex. "{x. x=0} <= {x. x <= 1}" -set2pred-> "x=0 --> x <= 1"              **)

           (EVERY [rtac subsetI i, 
                   rtac CollectI i,
                   dtac CollectD i,
                   (TRY(split_all_tac i)) THEN_MAYBE
                   ((rename_tac var_string i) THEN
-                   (full_simp_tac (HOL_basic_ss addsimps [split]) i)) ])) thm
+                   (full_simp_tac (HOL_basic_ss addsimps [split_conv]) i)) ])) thm
       end;
 
 (*****************************************************************************)
 (** BasicSimpTac is called to simplify all verification conditions. It does **)
 (** a light simplification by applying "mem_Collect_eq", then it calls      **)

 
 fun MaxSimpTac tac = FIRST'[rtac subset_refl, set2pred THEN_MAYBE' tac];
 
 fun BasicSimpTac tac =
   simp_tac
-    (HOL_basic_ss addsimps [mem_Collect_eq,split] addsimprocs [record_simproc])
+    (HOL_basic_ss addsimps [mem_Collect_eq,split_conv] addsimprocs [record_simproc])
   THEN_MAYBE' MaxSimpTac tac;
 
 (** HoareRuleTac **)
 
 fun WlpTac Mlem tac i = rtac SeqRule i THEN  HoareRuleTac Mlem tac false (i+1)