# HG changeset patch
# User haftmann
# Date 1277730187 -7200
# Node ID d3daea901123646e8bb973955af33adcf7f86177
# Parent  180e80b4eac1fb532b59b06ec54fa59f74968c7e
merged constants "split" and "prod_case"

diff -r 180e80b4eac1 -r d3daea901123 NEWS
--- a/NEWS	Mon Jun 28 15:03:07 2010 +0200
+++ b/NEWS	Mon Jun 28 15:03:07 2010 +0200
@@ -17,6 +17,10 @@
 
 *** HOL ***
 
+* Constant "split" has been merged with constant "prod_case";  names
+of ML functions, facts etc. involving split have been retained so far,
+though.  INCOMPATIBILITY.
+
 * Some previously unqualified names have been qualified:
 
   types
diff -r 180e80b4eac1 -r d3daea901123 src/HOL/Hoare/Hoare_Logic.thy
--- a/src/HOL/Hoare/Hoare_Logic.thy	Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Hoare/Hoare_Logic.thy	Mon Jun 28 15:03:07 2010 +0200
@@ -68,7 +68,7 @@
 
 fun mk_abstuple [x] body = abs (x, body)
   | mk_abstuple (x::xs) body =
-      Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body);
+      Syntax.const @{const_syntax prod_case} $ abs (x, mk_abstuple xs body);
 
 fun mk_fbody a e [x as (b,_)] = if a=b then e else Syntax.free b
   | mk_fbody a e ((b,_)::xs) =
@@ -128,21 +128,21 @@
 
 (*** print translations ***)
 ML{*
-fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) =
+fun dest_abstuple (Const (@{const_syntax prod_case},_) $ (Abs(v,_, body))) =
                             subst_bound (Syntax.free v, dest_abstuple body)
   | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
   | dest_abstuple trm = trm;
 
-fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
+fun abs2list (Const (@{const_syntax prod_case},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
   | abs2list (Abs(x,T,t)) = [Free (x, T)]
   | abs2list _ = [];
 
-fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t
+fun mk_ts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = mk_ts t
   | mk_ts (Abs(x,_,t)) = mk_ts t
   | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
   | mk_ts t = [t];
 
-fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) =
+fun mk_vts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) =
            ((Syntax.free x)::(abs2list t), mk_ts t)
   | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
   | mk_vts t = raise Match;
@@ -152,7 +152,7 @@
       if t = Bound i then find_ch vts (i-1) xs
       else (true, (v, subst_bounds (xs, t)));
 
-fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true
+fun is_f (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = true
   | is_f (Abs(x,_,t)) = true
   | is_f t = false;
 *}
diff -r 180e80b4eac1 -r d3daea901123 src/HOL/Hoare/Hoare_Logic_Abort.thy
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Mon Jun 28 15:03:07 2010 +0200
@@ -70,7 +70,7 @@
 
 fun mk_abstuple [x] body = abs (x, body)
   | mk_abstuple (x::xs) body =
-      Syntax.const @{const_syntax split} $ abs (x, mk_abstuple xs body);
+      Syntax.const @{const_syntax prod_case} $ abs (x, mk_abstuple xs body);
 
 fun mk_fbody a e [x as (b,_)] = if a=b then e else free b
   | mk_fbody a e ((b,_)::xs) =
@@ -130,21 +130,21 @@
 
 (*** print translations ***)
 ML{*
-fun dest_abstuple (Const (@{const_syntax split},_) $ (Abs(v,_, body))) =
+fun dest_abstuple (Const (@{const_syntax prod_case},_) $ (Abs(v,_, body))) =
       subst_bound (Syntax.free v, dest_abstuple body)
   | dest_abstuple (Abs(v,_, body)) = subst_bound (Syntax.free v, body)
   | dest_abstuple trm = trm;
 
-fun abs2list (Const (@{const_syntax split},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
+fun abs2list (Const (@{const_syntax prod_case},_) $ (Abs(x,T,t))) = Free (x, T)::abs2list t
   | abs2list (Abs(x,T,t)) = [Free (x, T)]
   | abs2list _ = [];
 
-fun mk_ts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = mk_ts t
+fun mk_ts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = mk_ts t
   | mk_ts (Abs(x,_,t)) = mk_ts t
   | mk_ts (Const (@{const_syntax Pair},_) $ a $ b) = a::(mk_ts b)
   | mk_ts t = [t];
 
-fun mk_vts (Const (@{const_syntax split},_) $ (Abs(x,_,t))) =
+fun mk_vts (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) =
            ((Syntax.free x)::(abs2list t), mk_ts t)
   | mk_vts (Abs(x,_,t)) = ([Syntax.free x], [t])
   | mk_vts t = raise Match;
@@ -154,7 +154,7 @@
       if t = Bound i then find_ch vts (i-1) xs
       else (true, (v, subst_bounds (xs,t)));
 
-fun is_f (Const (@{const_syntax split},_) $ (Abs(x,_,t))) = true
+fun is_f (Const (@{const_syntax prod_case},_) $ (Abs(x,_,t))) = true
   | is_f (Abs(x,_,t)) = true
   | is_f t = false;
 *}
diff -r 180e80b4eac1 -r d3daea901123 src/HOL/Hoare/hoare_tac.ML
--- a/src/HOL/Hoare/hoare_tac.ML	Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML	Mon Jun 28 15:03:07 2010 +0200
@@ -16,7 +16,7 @@
 local open HOLogic in
 
 (** maps (%x1 ... xn. t) to [x1,...,xn] **)
-fun abs2list (Const (@{const_name split}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
+fun abs2list (Const (@{const_name prod_case}, _) $ Abs (x, T, t)) = Free (x, T) :: abs2list t
   | abs2list (Abs (x, T, t)) = [Free (x, T)]
   | abs2list _ = [];
 
@@ -32,7 +32,7 @@
         else let val z  = mk_abstupleC w body;
                  val T2 = case z of Abs(_,T,_) => T
                         | Const (_, Type (_,[_, Type (_,[T,_])])) $ _ => T;
-       in Const (@{const_name split}, (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT)
+       in Const (@{const_name prod_case}, (T --> T2 --> boolT) --> mk_prodT (T,T2) --> boolT)
           $ absfree (n, T, z) end end;
 
 (** maps [x1,...,xn] to (x1,...,xn) and types**)
diff -r 180e80b4eac1 -r d3daea901123 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jun 28 15:03:07 2010 +0200
@@ -379,7 +379,7 @@
         from this Inl 1(1) exec_f mrec show ?thesis
         proof (cases "ret_mrec")
           case (Inl aaa)
-          from this mrec exec_f Inl' Inr' 1(1) mrec_rec 1(2)[OF exec_f Inl' Inr', of "aaa" "h2"] 1(3)
+          from this mrec exec_f Inl' Inr' 1(1) mrec_rec 1(2) [OF exec_f [symmetric] Inl' Inr', of "aaa" "h2"] 1(3)
             show ?thesis
               apply auto
               apply (rule rec_case)
diff -r 180e80b4eac1 -r d3daea901123 src/HOL/Import/HOL/pair.imp
--- a/src/HOL/Import/HOL/pair.imp	Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Import/HOL/pair.imp	Mon Jun 28 15:03:07 2010 +0200
@@ -10,8 +10,8 @@
   "prod" > "Product_Type.*"
 
 const_maps
-  "pair_case" > "Product_Type.split"
-  "UNCURRY" > "Product_Type.split"
+  "pair_case" > "Product_Type.prod_case"
+  "UNCURRY" > "Product_Type.prod_case"
   "FST" > "Product_Type.fst"
   "SND" > "Product_Type.snd"
   "RPROD" > "HOL4Base.pair.RPROD"
diff -r 180e80b4eac1 -r d3daea901123 src/HOL/Library/AssocList.thy
--- a/src/HOL/Library/AssocList.thy	Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Library/AssocList.thy	Mon Jun 28 15:03:07 2010 +0200
@@ -427,8 +427,7 @@
 
 lemma merge_updates:
   "merge qs ps = updates (rev (map fst ps)) (rev (map snd ps)) qs"
-  by (simp add: merge_def updates_def split_prod_case
-    foldr_fold_rev zip_rev zip_map_fst_snd)
+  by (simp add: merge_def updates_def foldr_fold_rev zip_rev zip_map_fst_snd)
 
 lemma dom_merge: "fst ` set (merge xs ys) = fst ` set xs \<union> fst ` set ys"
   by (induct ys arbitrary: xs) (auto simp add: dom_update)
@@ -449,7 +448,7 @@
     More_List.fold (\<lambda>(k, v) m. m(k \<mapsto> v)) (rev ys) \<circ> map_of"
     by (rule fold_apply) (simp add: update_conv' prod_case_beta split_def expand_fun_eq)
   then show ?thesis
-    by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev split_prod_case expand_fun_eq)
+    by (simp add: merge_def map_add_map_of_foldr foldr_fold_rev expand_fun_eq)
 qed
 
 corollary merge_conv:
diff -r 180e80b4eac1 -r d3daea901123 src/HOL/Library/Nat_Bijection.thy
--- a/src/HOL/Library/Nat_Bijection.thy	Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Library/Nat_Bijection.thy	Mon Jun 28 15:03:07 2010 +0200
@@ -213,6 +213,7 @@
 termination list_decode
 apply (relation "measure id", simp_all)
 apply (drule arg_cong [where f="prod_encode"])
+apply (drule sym)
 apply (simp add: le_imp_less_Suc le_prod_encode_2)
 done
 
diff -r 180e80b4eac1 -r d3daea901123 src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Mon Jun 28 15:03:07 2010 +0200
@@ -18,7 +18,7 @@
 
 section {* Pairs *}
 
-setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name split}] *}
+setup {* Predicate_Compile_Data.ignore_consts [@{const_name fst}, @{const_name snd}, @{const_name prod_case}] *}
 
 section {* Bounded quantifiers *}
 
diff -r 180e80b4eac1 -r d3daea901123 src/HOL/Library/RBT_Impl.thy
--- a/src/HOL/Library/RBT_Impl.thy	Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Library/RBT_Impl.thy	Mon Jun 28 15:03:07 2010 +0200
@@ -1076,7 +1076,7 @@
   from this Empty_is_rbt have
     "lookup (More_List.fold (prod_case insert) (rev xs) Empty) = lookup Empty ++ map_of xs"
      by (simp add: `ys = rev xs`)
-  then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_fold_rev prod_case_split)
+  then show ?thesis by (simp add: bulkload_def lookup_Empty foldr_fold_rev)
 qed
 
 hide_const (open) Empty insert delete entries keys bulkload lookup map_entry map fold union sorted
diff -r 180e80b4eac1 -r d3daea901123 src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Mon Jun 28 15:03:07 2010 +0200
@@ -323,7 +323,7 @@
     let val VarAbs = Syntax.variant_abs(s,tp,trm);
     in get_decls sign (Const(fst VarAbs,tp)::Clist) (snd VarAbs)
     end
-  | get_decls sign Clist ((Const (@{const_name split}, _)) $ trm) = get_decls sign Clist trm
+  | get_decls sign Clist ((Const (@{const_name prod_case}, _)) $ trm) = get_decls sign Clist trm
   | get_decls sign Clist trm = (Clist,trm);
 
 fun make_mu_def sign ((tt $ LHS) $ (ttt $ RHS)) =
@@ -389,7 +389,7 @@
       val t2 = t1 $ ParamDeclTerm
   in t2 end;
 
-fun is_fundef (Const("==", _) $ _ $ (Const (@{const_name split}, _) $ _)) = true
+fun is_fundef (Const("==", _) $ _ $ (Const (@{const_name prod_case}, _) $ _)) = true
   | is_fundef (Const("==", _) $ _ $ Abs _) = true 
   | is_fundef _ = false; 
 
diff -r 180e80b4eac1 -r d3daea901123 src/HOL/Probability/Borel.thy
--- a/src/HOL/Probability/Borel.thy	Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Probability/Borel.thy	Mon Jun 28 15:03:07 2010 +0200
@@ -203,7 +203,7 @@
         by (metis surj_def)
 
       from Fract i j n show ?thesis
-        by (metis prod.cases prod_case_split)
+        by (metis prod.cases)
   qed
 qed
 
diff -r 180e80b4eac1 -r d3daea901123 src/HOL/Probability/Caratheodory.thy
--- a/src/HOL/Probability/Caratheodory.thy	Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Probability/Caratheodory.thy	Mon Jun 28 15:03:07 2010 +0200
@@ -829,7 +829,7 @@
         with sbBB [of i] obtain j where "x \<in> BB i j"
           by blast        
         thus "\<exists>i. x \<in> split BB (prod_decode i)"
-          by (metis prod_encode_inverse prod.cases prod_case_split)
+          by (metis prod_encode_inverse prod.cases)
       qed 
     have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
       by (rule ext)  (auto simp add: C_def) 
diff -r 180e80b4eac1 -r d3daea901123 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Product_Type.thy	Mon Jun 28 15:03:07 2010 +0200
@@ -163,8 +163,8 @@
 
 subsubsection {* Tuple syntax *}
 
-definition split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
-  split_prod_case: "split == prod_case"
+abbreviation (input) split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
+  "split \<equiv> prod_case"
 
 text {*
   Patterns -- extends pre-defined type @{typ pttrn} used in
@@ -185,8 +185,8 @@
 translations
   "(x, y)" == "CONST Pair x y"
   "_tuple x (_tuple_args y z)" == "_tuple x (_tuple_arg (_tuple y z))"
-  "%(x, y, zs). b" == "CONST split (%x (y, zs). b)"
-  "%(x, y). b" == "CONST split (%x y. b)"
+  "%(x, y, zs). b" == "CONST prod_case (%x (y, zs). b)"
+  "%(x, y). b" == "CONST prod_case (%x y. b)"
   "_abs (CONST Pair x y) t" => "%(x, y). t"
   -- {* The last rule accommodates tuples in `case C ... (x,y) ... => ...'
      The (x,y) is parsed as `Pair x y' because it is logic, not pttrn *}
@@ -204,7 +204,7 @@
           Syntax.const @{syntax_const "_abs"} $
             (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
         end
-    | split_tr' [Abs (x, T, (s as Const (@{const_syntax split}, _) $ t))] =
+    | split_tr' [Abs (x, T, (s as Const (@{const_syntax prod_case}, _) $ t))] =
         (* split (%x. (split (%y z. t))) => %(x,y,z). t *)
         let
           val Const (@{syntax_const "_abs"}, _) $
@@ -215,7 +215,7 @@
             (Syntax.const @{syntax_const "_pattern"} $ x' $
               (Syntax.const @{syntax_const "_patterns"} $ y $ z)) $ t''
         end
-    | split_tr' [Const (@{const_syntax split}, _) $ t] =
+    | split_tr' [Const (@{const_syntax prod_case}, _) $ t] =
         (* split (split (%x y z. t)) => %((x, y), z). t *)
         split_tr' [(split_tr' [t])] (* inner split_tr' creates next pattern *)
     | split_tr' [Const (@{syntax_const "_abs"}, _) $ x_y $ Abs abs] =
@@ -225,7 +225,7 @@
             (Syntax.const @{syntax_const "_pattern"} $ x_y $ z) $ t
         end
     | split_tr' _ = raise Match;
-in [(@{const_syntax split}, split_tr')] end
+in [(@{const_syntax prod_case}, split_tr')] end
 *}
 
 (* print "split f" as "\<lambda>(x,y). f x y" and "split (\<lambda>x. f x)" as "\<lambda>(x,y). f x y" *) 
@@ -234,7 +234,7 @@
   fun split_guess_names_tr' _ T [Abs (x, _, Abs _)] = raise Match
     | split_guess_names_tr' _ T [Abs (x, xT, t)] =
         (case (head_of t) of
-          Const (@{const_syntax split}, _) => raise Match
+          Const (@{const_syntax prod_case}, _) => raise Match
         | _ =>
           let 
             val (_ :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
@@ -246,7 +246,7 @@
           end)
     | split_guess_names_tr' _ T [t] =
         (case head_of t of
-          Const (@{const_syntax split}, _) => raise Match
+          Const (@{const_syntax prod_case}, _) => raise Match
         | _ =>
           let
             val (xT :: yT :: _) = binder_types (domain_type T) handle Bind => raise Match;
@@ -257,21 +257,12 @@
               (Syntax.const @{syntax_const "_pattern"} $ x' $ y) $ t''
           end)
     | split_guess_names_tr' _ _ _ = raise Match;
-in [(@{const_syntax split}, split_guess_names_tr')] end
+in [(@{const_syntax prod_case}, split_guess_names_tr')] end
 *}
 
 
 subsubsection {* Code generator setup *}
 
-lemma split_case_cert:
-  assumes "CASE \<equiv> split f"
-  shows "CASE (a, b) \<equiv> f a b"
-  using assms by (simp add: split_prod_case)
-
-setup {*
-  Code.add_case @{thm split_case_cert}
-*}
-
 code_type *
   (SML infix 2 "*")
   (OCaml infix 2 "*")
@@ -315,7 +306,7 @@
         val s' = Codegen.new_name t s;
         val v = Free (s', T)
       in apfst (cons v) (strip_abs_split (i-1) (subst_bound (v, t))) end
-  | strip_abs_split i (u as Const (@{const_name split}, _) $ t) =
+  | strip_abs_split i (u as Const (@{const_name prod_case}, _) $ t) =
       (case strip_abs_split (i+1) t of
         (v :: v' :: vs, u) => (HOLogic.mk_prod (v, v') :: vs, u)
       | _ => ([], u))
@@ -357,7 +348,7 @@
   | _ => NONE);
 
 fun split_codegen thy defs dep thyname brack t gr = (case strip_comb t of
-    (t1 as Const (@{const_name split}, _), t2 :: ts) =>
+    (t1 as Const (@{const_name prod_case}, _), t2 :: ts) =>
       let
         val ([p], u) = strip_abs_split 1 (t1 $ t2);
         val (q, gr1) = Codegen.invoke_codegen thy defs dep thyname false p gr;
@@ -421,7 +412,7 @@
   by (simp add: Pair_fst_snd_eq)
 
 lemma split_conv [simp, code]: "split f (a, b) = f a b"
-  by (simp add: split_prod_case)
+  by (fact prod.cases)
 
 lemma splitI: "f a b \<Longrightarrow> split f (a, b)"
   by (rule split_conv [THEN iffD2])
@@ -430,11 +421,11 @@
   by (rule split_conv [THEN iffD1])
 
 lemma split_Pair [simp]: "(\<lambda>(x, y). (x, y)) = id"
-  by (simp add: split_prod_case expand_fun_eq split: prod.split)
+  by (simp add: expand_fun_eq split: prod.split)
 
 lemma split_eta: "(\<lambda>(x, y). f (x, y)) = f"
   -- {* Subsumes the old @{text split_Pair} when @{term f} is the identity function. *}
-  by (simp add: split_prod_case expand_fun_eq split: prod.split)
+  by (simp add: expand_fun_eq split: prod.split)
 
 lemma split_comp: "split (f \<circ> g) x = f (g (fst x)) (snd x)"
   by (cases x) simp
@@ -443,7 +434,7 @@
   by (cases p) simp
 
 lemma The_split: "The (split P) = (THE xy. P (fst xy) (snd xy))"
-  by (simp add: split_prod_case prod_case_unfold)
+  by (simp add: prod_case_unfold)
 
 lemma split_weak_cong: "p = q \<Longrightarrow> split c p = split c q"
   -- {* Prevents simplification of @{term c}: much faster *}
@@ -529,7 +520,7 @@
     | no_args k i (Bound m) = m < k orelse m > k + i
     | no_args _ _ _ = true;
   fun split_pat tp i (Abs  (_, _, t)) = if tp 0 i t then SOME (i, t) else NONE
-    | split_pat tp i (Const (@{const_name split}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
+    | split_pat tp i (Const (@{const_name prod_case}, _) $ Abs (_, _, t)) = split_pat tp (i + 1) t
     | split_pat tp i _ = NONE;
   fun metaeq ss lhs rhs = mk_meta_eq (Goal.prove (Simplifier.the_context ss) [] []
         (HOLogic.mk_Trueprop (HOLogic.mk_eq (lhs, rhs)))
@@ -546,12 +537,12 @@
         if Pair_pat k i (t $ u) then incr_boundvars k arg
         else (subst arg k i t $ subst arg k i u)
     | subst arg k i t = t;
-  fun beta_proc ss (s as Const (@{const_name split}, _) $ Abs (_, _, t) $ arg) =
+  fun beta_proc ss (s as Const (@{const_name prod_case}, _) $ Abs (_, _, t) $ arg) =
         (case split_pat beta_term_pat 1 t of
           SOME (i, f) => SOME (metaeq ss s (subst arg 0 i f))
         | NONE => NONE)
     | beta_proc _ _ = NONE;
-  fun eta_proc ss (s as Const (@{const_name split}, _) $ Abs (_, _, t)) =
+  fun eta_proc ss (s as Const (@{const_name prod_case}, _) $ Abs (_, _, t)) =
         (case split_pat eta_term_pat 1 t of
           SOME (_, ft) => SOME (metaeq ss s (let val (f $ arg) = ft in f end))
         | NONE => NONE)
@@ -598,10 +589,10 @@
   done
 
 lemma splitE: "split c p ==> (!!x y. p = (x, y) ==> c x y ==> Q) ==> Q"
-  by (induct p) (auto simp add: split_prod_case)
+  by (induct p) auto
 
 lemma splitE': "split c p z ==> (!!x y. p = (x, y) ==> c x y z ==> Q) ==> Q"
-  by (induct p) (auto simp add: split_prod_case)
+  by (induct p) auto
 
 lemma splitE2:
   "[| Q (split P z);  !!x y. [|z = (x, y); Q (P x y)|] ==> R |] ==> R"
@@ -627,14 +618,14 @@
   assumes major: "z \<in> split c p"
     and cases: "\<And>x y. p = (x, y) \<Longrightarrow> z \<in> c x y \<Longrightarrow> Q"
   shows Q
-  by (rule major [unfolded split_prod_case prod_case_unfold] cases surjective_pairing)+
+  by (rule major [unfolded prod_case_unfold] cases surjective_pairing)+
 
 declare mem_splitI2 [intro!] mem_splitI [intro!] splitI2' [intro!] splitI2 [intro!] splitI [intro!]
 declare mem_splitE [elim!] splitE' [elim!] splitE [elim!]
 
 ML {*
 local (* filtering with exists_p_split is an essential optimization *)
-  fun exists_p_split (Const (@{const_name split},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
+  fun exists_p_split (Const (@{const_name prod_case},_) $ _ $ (Const (@{const_name Pair},_)$_$_)) = true
     | exists_p_split (t $ u) = exists_p_split t orelse exists_p_split u
     | exists_p_split (Abs (_, _, t)) = exists_p_split t
     | exists_p_split _ = false;
@@ -712,13 +703,9 @@
 declare prod_caseI2' [intro!] prod_caseI2 [intro!] prod_caseI [intro!]
 declare prod_caseE' [elim!] prod_caseE [elim!]
 
-lemma prod_case_split:
-  "prod_case = split"
-  by (auto simp add: expand_fun_eq)
-
 lemma prod_case_beta:
   "prod_case f p = f (fst p) (snd p)"
-  unfolding prod_case_split split_beta ..
+  by (fact split_beta)
 
 lemma prod_cases3 [cases type]:
   obtains (fields) a b c where "y = (a, b, c)"
@@ -762,7 +749,7 @@
 
 lemma split_def:
   "split = (\<lambda>c p. c (fst p) (snd p))"
-  unfolding split_prod_case prod_case_unfold ..
+  by (fact prod_case_unfold)
 
 definition internal_split :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c" where
   "internal_split == split"
diff -r 180e80b4eac1 -r d3daea901123 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Jun 28 15:03:07 2010 +0200
@@ -2080,7 +2080,7 @@
     list_abs (outer,
               Const (@{const_name Image}, uncurried_T --> set_T --> set_T)
               $ (Const (@{const_name rtrancl}, uncurried_T --> uncurried_T)
-                 $ (Const (@{const_name split}, curried_T --> uncurried_T)
+                 $ (Const (@{const_name prod_case}, curried_T --> uncurried_T)
                     $ list_comb (Const step_x, outer_bounds)))
               $ list_comb (Const base_x, outer_bounds)
               |> ap_curry tuple_arg_Ts tuple_T)
diff -r 180e80b4eac1 -r d3daea901123 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Mon Jun 28 15:03:07 2010 +0200
@@ -2015,7 +2015,7 @@
   | split_lambda (Const ("Product_Type.Unity", _)) t = Abs ("x", HOLogic.unitT, t)
   | split_lambda t _ = raise (TERM ("split_lambda", [t]))
 
-fun strip_split_abs (Const (@{const_name split}, _) $ t) = strip_split_abs t
+fun strip_split_abs (Const (@{const_name prod_case}, _) $ t) = strip_split_abs t
   | strip_split_abs (Abs (_, _, t)) = strip_split_abs t
   | strip_split_abs t = t
 
diff -r 180e80b4eac1 -r d3daea901123 src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML	Mon Jun 28 15:03:07 2010 +0200
@@ -179,7 +179,7 @@
               |> maps (fn (res, (names, prems)) =>
                 flatten' (betapply (g, res)) (names, prems))
             end)
-        | Const (@{const_name split}, _) => 
+        | Const (@{const_name prod_case}, _) => 
             (let
               val (_, g :: res :: args) = strip_comb t
               val [res1, res2] = Name.variant_list names ["res1", "res2"]
diff -r 180e80b4eac1 -r d3daea901123 src/HOL/Tools/Quotient/quotient_term.ML
--- a/src/HOL/Tools/Quotient/quotient_term.ML	Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML	Mon Jun 28 15:03:07 2010 +0200
@@ -560,12 +560,12 @@
            end
        end
 
-  | (((t1 as Const (@{const_name split}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
-     ((t2 as Const (@{const_name split}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
+  | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, Abs(v1', ty', s1))),
+     ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , Abs(v2', _  , s2)))) =>
        regularize_trm ctxt (t1, t2) $ Abs (v1, ty, Abs (v1', ty', regularize_trm ctxt (s1, s2)))
 
-  | (((t1 as Const (@{const_name split}, _)) $ Abs (v1, ty, s1)),
-     ((t2 as Const (@{const_name split}, _)) $ Abs (v2, _ , s2))) =>
+  | (((t1 as Const (@{const_name prod_case}, _)) $ Abs (v1, ty, s1)),
+     ((t2 as Const (@{const_name prod_case}, _)) $ Abs (v2, _ , s2))) =>
        regularize_trm ctxt (t1, t2) $ Abs (v1, ty, regularize_trm ctxt (s1, s2))
 
   | (t1 $ t2, t1' $ t2') =>
diff -r 180e80b4eac1 -r d3daea901123 src/HOL/Tools/TFL/usyntax.ML
--- a/src/HOL/Tools/TFL/usyntax.ML	Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML	Mon Jun 28 15:03:07 2010 +0200
@@ -196,7 +196,7 @@
 
 local
 fun mk_uncurry (xt, yt, zt) =
-    Const(@{const_name split}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
+    Const(@{const_name prod_case}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
 fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
   | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
 fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
@@ -276,7 +276,7 @@
   | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
 
 
-local  fun ucheck t = (if #Name (dest_const t) = @{const_name split} then t
+local  fun ucheck t = (if #Name (dest_const t) = @{const_name prod_case} then t
                        else raise Match)
 in
 fun dest_pabs used tm =
diff -r 180e80b4eac1 -r d3daea901123 src/HOL/Tools/hologic.ML
--- a/src/HOL/Tools/hologic.ML	Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Tools/hologic.ML	Mon Jun 28 15:03:07 2010 +0200
@@ -315,12 +315,12 @@
   end;
 
 fun split_const (A, B, C) =
-  Const ("Product_Type.split", (A --> B --> C) --> mk_prodT (A, B) --> C);
+  Const ("Product_Type.prod.prod_case", (A --> B --> C) --> mk_prodT (A, B) --> C);
 
 fun mk_split t =
   (case Term.fastype_of t of
     T as (Type ("fun", [A, Type ("fun", [B, C])])) =>
-      Const ("Product_Type.split", T --> mk_prodT (A, B) --> C) $ t
+      Const ("Product_Type.prod.prod_case", T --> mk_prodT (A, B) --> C) $ t
   | _ => raise TERM ("mk_split: bad body type", [t]));
 
 (*Maps the type T1 * ... * Tn to [T1, ..., Tn], however nested*)
@@ -427,7 +427,7 @@
 val strip_psplits =
   let
     fun strip [] qs Ts t = (t, rev Ts, qs)
-      | strip (p :: ps) qs Ts (Const ("Product_Type.split", _) $ t) =
+      | strip (p :: ps) qs Ts (Const ("Product_Type.prod.prod_case", _) $ t) =
           strip ((1 :: p) :: (2 :: p) :: ps) (p :: qs) Ts t
       | strip (p :: ps) qs Ts (Abs (s, T, t)) = strip ps qs (T :: Ts) t
       | strip (p :: ps) qs Ts t = strip ps qs
diff -r 180e80b4eac1 -r d3daea901123 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Mon Jun 28 15:03:07 2010 +0200
@@ -374,7 +374,7 @@
     fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
       liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
     fun mk_split T = Sign.mk_const thy
-      (@{const_name split}, [T, @{typ "unit => term"}, liftT @{typ "term list option"} @{typ Random.seed}]);
+      (@{const_name prod_case}, [T, @{typ "unit => term"}, liftT @{typ "term list option"} @{typ Random.seed}]);
     fun mk_scomp_split T t t' =
       mk_scomp (mk_termtyp T) @{typ "term list option"} @{typ Random.seed} t
         (mk_split T $ Abs ("", T, Abs ("", @{typ "unit => term"}, t')));
@@ -414,7 +414,7 @@
     fun mk_scomp T1 T2 sT f g = Const (@{const_name scomp},
       liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g;
     fun mk_split T = Sign.mk_const thy
-      (@{const_name split}, [T, @{typ "unit => term"},
+      (@{const_name prod_case}, [T, @{typ "unit => term"},
         liftT @{typ "term list option * (bool list * bool)"} @{typ Random.seed}]);
     fun mk_scomp_split T t t' =
       mk_scomp (mk_termtyp T) @{typ "term list option * (bool list * bool)"} @{typ Random.seed} t
diff -r 180e80b4eac1 -r d3daea901123 src/HOL/Word/Num_Lemmas.thy
--- a/src/HOL/Word/Num_Lemmas.thy	Mon Jun 28 15:03:07 2010 +0200
+++ b/src/HOL/Word/Num_Lemmas.thy	Mon Jun 28 15:03:07 2010 +0200
@@ -11,8 +11,8 @@
 lemma contentsI: "y = {x} ==> contents y = x" 
   unfolding contents_def by auto -- {* FIXME move *}
 
-lemmas split_split = prod.split [unfolded prod_case_split]
-lemmas split_split_asm = prod.split_asm [unfolded prod_case_split]
+lemmas split_split = prod.split
+lemmas split_split_asm = prod.split_asm
 lemmas split_splits = split_split split_split_asm
 
 lemmas funpow_0 = funpow.simps(1)