diff -r 9b6a0fb85fa3 -r c3658c18b7bc src/Doc/Main/Main_Doc.thy
--- a/src/Doc/Main/Main_Doc.thy	Tue Oct 13 09:21:14 2015 +0200
+++ b/src/Doc/Main/Main_Doc.thy	Tue Oct 13 09:21:15 2015 +0200
@@ -218,7 +218,7 @@
 @{const Pair} & @{typeof Pair}\\
 @{const fst} & @{typeof fst}\\
 @{const snd} & @{typeof snd}\\
-@{const split} & @{typeof split}\\
+@{const case_prod} & @{typeof case_prod}\\
 @{const curry} & @{typeof curry}\\
 @{const Product_Type.Sigma} & @{term_type_only Product_Type.Sigma "'a set\<Rightarrow>('a\<Rightarrow>'b set)\<Rightarrow>('a*'b)set"}\\
 \end{supertabular}
@@ -227,7 +227,7 @@
 
 \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}}
 @{term"Pair a b"} & @{term[source]"Pair a b"}\\
-@{term"split (\<lambda>x y. t)"} & @{term[source]"split (\<lambda>x y. t)"}\\
+@{term"case_prod (\<lambda>x y. t)"} & @{term[source]"case_prod (\<lambda>x y. t)"}\\
 @{term"A <*> B"} &  @{text"Sigma A (\<lambda>\<^raw:\_>. B)"} & (\verb$<*>$)
 \end{tabular}