--- a/doc-src/TutorialI/Types/document/Pairs.tex Wed Apr 16 21:53:05 2008 +0200
+++ b/doc-src/TutorialI/Types/document/Pairs.tex Wed Apr 16 22:17:43 2008 +0200
@@ -104,7 +104,7 @@
If we consider why this lemma presents a problem,
we quickly realize that we need to replace the variable~\isa{p} by some pair \isa{{\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}}. Then both sides of the
equation would simplify to \isa{a} by the simplification rules
-\isa{split\ c\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ c\ a\ b} and \isa{fst\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ a}.
+\isa{split\ f\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ f\ a\ b} and \isa{fst\ {\isacharparenleft}a{\isacharcomma}\ b{\isacharparenright}\ {\isacharequal}\ a}.
To reason about tuple patterns requires some way of
converting a variable of product type into a pair.