--- a/src/HOLCF/Sprod.thy Fri Oct 22 15:47:43 2010 -0700
+++ b/src/HOLCF/Sprod.thy Fri Oct 22 15:49:18 2010 -0700
@@ -144,7 +144,7 @@
lemma ssnd_defined: "p \<noteq> \<bottom> \<Longrightarrow> ssnd\<cdot>p \<noteq> \<bottom>"
by simp
-lemma surjective_pairing_Sprod2: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p"
+lemma spair_sfst_ssnd: "(:sfst\<cdot>p, ssnd\<cdot>p:) = p"
by (cases p, simp_all)
lemma below_sprod: "x \<sqsubseteq> y = (sfst\<cdot>x \<sqsubseteq> sfst\<cdot>y \<and> ssnd\<cdot>x \<sqsubseteq> ssnd\<cdot>y)"