--- a/doc-src/TutorialI/Types/Pairs.thy Wed Dec 13 09:32:55 2000 +0100
+++ b/doc-src/TutorialI/Types/Pairs.thy Wed Dec 13 09:39:53 2000 +0100
@@ -39,7 +39,8 @@
different terms).
Internally, @{term"%(x,y). t"} becomes @{text"split (\<lambda>x y. t)"}, where
-@{term split} is the uncurrying function of type @{text"('a \<Rightarrow> 'b
+@{term split}\indexbold{*split (constant)}
+is the uncurrying function of type @{text"('a \<Rightarrow> 'b
\<Rightarrow> 'c) \<Rightarrow> 'a \<times> 'b \<Rightarrow> 'c"} defined as
\begin{center}
@{thm split_def}
@@ -78,7 +79,7 @@
*}
lemma "(\<lambda>(x,y).y) p = snd p"
-apply(simp only: split:split_split);
+apply(split split_split);
txt{*
@{subgoals[display,indent=0]}
@@ -191,10 +192,10 @@
In case you would like to turn off this automatic splitting, just disable the
responsible simplification rules:
\begin{center}
-@{thm split_paired_All}
+@{thm split_paired_All[no_vars]}
\hfill
(@{thm[source]split_paired_All})\\
-@{thm split_paired_Ex}
+@{thm split_paired_Ex[no_vars]}
\hfill
(@{thm[source]split_paired_Ex})
\end{center}