1.1 --- a/src/Doc/Main/Main_Doc.thy	Tue Oct 13 09:21:14 2015 +0200
     1.2 +++ b/src/Doc/Main/Main_Doc.thy	Tue Oct 13 09:21:15 2015 +0200
     1.3 @@ -218,7 +218,7 @@
     1.4  @{const Pair} & @{typeof Pair}\\
     1.5  @{const fst} & @{typeof fst}\\
     1.6  @{const snd} & @{typeof snd}\\
     1.7 -@{const split} & @{typeof split}\\
     1.8 +@{const case_prod} & @{typeof case_prod}\\
     1.9  @{const curry} & @{typeof curry}\\
    1.10  @{const Product_Type.Sigma} & @{term_type_only Product_Type.Sigma "'a set\<Rightarrow>('a\<Rightarrow>'b set)\<Rightarrow>('a*'b)set"}\\
    1.11  \end{supertabular}
    1.12 @@ -227,7 +227,7 @@
    1.13  
    1.14  \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}}
    1.15  @{term"Pair a b"} & @{term[source]"Pair a b"}\\
    1.16 -@{term"split (\<lambda>x y. t)"} & @{term[source]"split (\<lambda>x y. t)"}\\
    1.17 +@{term"case_prod (\<lambda>x y. t)"} & @{term[source]"case_prod (\<lambda>x y. t)"}\\
    1.18  @{term"A <*> B"} &  @{text"Sigma A (\<lambda>\<^raw:\_>. B)"} & (\verb$<*>$)
    1.19  \end{tabular}
    1.20