src/HOL/Product_Type.thy

--- a/src/HOL/Product_Type.thy	Tue Aug 16 15:36:28 2005 +0200
+++ b/src/HOL/Product_Type.thy	Tue Aug 16 18:53:11 2005 +0200
@@ -269,7 +269,8 @@
   -- {* Do not add as rewrite rule: invalidates some proofs in IMP *}
   by (cases p) simp
 
-declare surjective_pairing [symmetric, simp]
+lemmas pair_collapse = surjective_pairing [symmetric]
+declare pair_collapse [simp]
 
 lemma surj_pair [simp]: "EX x y. z = (x, y)"
   apply (rule exI)