--- a/src/HOL/Prod.ML Fri Jul 14 16:29:02 2000 +0200
+++ b/src/HOL/Prod.ML Fri Jul 14 16:32:44 2000 +0200
@@ -67,6 +67,7 @@
by (pair_tac "p" 1);
by (Asm_simp_tac 1);
qed "surjective_pairing";
+Addsimps [surjective_pairing RS sym];
Goal "? x y. z = (x, y)";
by (rtac exI 1);