src/HOL/HOLCF/Ssum.thy

--- a/src/HOL/HOLCF/Ssum.thy	Mon Aug 08 10:26:26 2011 -0700
+++ b/src/HOL/HOLCF/Ssum.thy	Mon Aug 08 10:32:55 2011 -0700
@@ -52,7 +52,7 @@
 
 lemmas Rep_ssum_simps =
   Rep_ssum_inject [symmetric] below_ssum_def
-  Pair_fst_snd_eq below_prod_def
+  prod_eq_iff below_prod_def
   Rep_ssum_strict Rep_ssum_sinl Rep_ssum_sinr
 
 subsection {* Properties of \emph{sinl} and \emph{sinr} *}