src/HOL/Product_Type.ML

 qed "split_paired_Ex";
 Addsimps [split_paired_Ex];
 
 Goalw [split_def] "split c (a,b) = c a b";
 by (Simp_tac 1);
-qed "split";
-Addsimps [split];
+qed "split_conv";
+Addsimps [split_conv];
+(*bind_thm ("split", split_conv);                  (*for compatibility*)*)
 
 (*Subsumes the old split_Pair when f is the identity function*)
 Goal "split (%x y. f(x,y)) = f";
 by (rtac ext 1);
 by (pair_tac "x" 1);

 qed "split_weak_cong";
 
 Goal "(%(x,y). f(x,y)) = f";
 by (rtac ext 1);
 by (split_all_tac 1);
-by (rtac split 1);
+by (rtac split_conv 1);
 qed "split_eta";
 
 val prems = Goal "(!!x y. f x y = g(x,y)) ==> (%(x,y). f x y) = g";
 by (asm_simp_tac (simpset() addsimps prems@[split_eta]) 1);
 qed "cond_split_eta";

 end;
 
 Addsimprocs [split_beta_proc,split_eta_proc];
 
 Goal "(%(x,y). P x y) z = P (fst z) (snd z)";
-by (stac surjective_pairing 1 THEN rtac split 1);
+by (stac surjective_pairing 1 THEN rtac split_conv 1);
 qed "split_beta";
 
 (*For use with split_tac and the simplifier*)
 Goal "R (split c p) = (! x y. p = (x,y) --> R (c x y))";
 by (stac surjective_pairing 1);
-by (stac split 1);
+by (stac split_conv 1);
 by (Blast_tac 1);
 qed "split_split";
 
 (* could be done after split_tac has been speeded up significantly:
 simpset_ref() := simpset() addsplits [split_split];

 by (REPEAT (resolve_tac (prems@[surjective_pairing]) 1));
 by (rtac (split_beta RS subst) 1 THEN rtac major 1);
 qed "splitE2";
 
 Goal "split R (a,b) ==> R a b";
-by (etac (split RS iffD1) 1);
+by (etac (split_conv RS iffD1) 1);
 qed "splitD";
 
 Goal "z: c a b ==> z: split c (a,b)";
 by (Asm_simp_tac 1);
 qed "mem_splitI";

 *)
 
 (*** prod_fun -- action of the product functor upon functions ***)
 
 Goalw [prod_fun_def] "prod_fun f g (a,b) = (f(a),g(b))";
-by (rtac split 1);
+by (rtac split_conv 1);
 qed "prod_fun";
 Addsimps [prod_fun];
 
 Goal "prod_fun (f1 o f2) (g1 o g2) = ((prod_fun f1 g1) o (prod_fun f2 g2))";
 by (rtac ext 1);

 by (Blast_tac 1);
 qed "Times_Diff_distrib1";
 
 
 (*Attempts to remove occurrences of split, and pair-valued parameters*)
-val remove_split = rewrite_rule [split RS eq_reflection] o split_all;
+val remove_split = rewrite_rule [split_conv RS eq_reflection] o split_all;
 
 local
 
 (*In ap_split S T u, term u expects separate arguments for the factors of S,
   with result type T.  The call creates a new term expecting one argument