--- a/src/HOLCF/Sprod3.thy Fri Oct 10 18:37:49 1997 +0200
+++ b/src/HOLCF/Sprod3.thy Fri Oct 10 19:02:28 1997 +0200
@@ -24,10 +24,10 @@
"(|x, y|)" == "spair`x`y"
defs
-spair_def "spair == (LAM x y.Ispair x y)"
-sfst_def "sfst == (LAM p.Isfst p)"
-ssnd_def "ssnd == (LAM p.Issnd p)"
-ssplit_def "ssplit == (LAM f. strictify`(LAM p.f`(sfst`p)`(ssnd`p)))"
+spair_def "spair == (LAM x y. Ispair x y)"
+sfst_def "sfst == (LAM p. Isfst p)"
+ssnd_def "ssnd == (LAM p. Issnd p)"
+ssplit_def "ssplit == (LAM f. strictify`(LAM p. f`(sfst`p)`(ssnd`p)))"
end