added (surjective_pairing RS sym) to simpset

--- a/src/HOL/AxClasses/Group/GroupDefs.ML	Fri Jul 14 16:29:02 2000 +0200
+++ b/src/HOL/AxClasses/Group/GroupDefs.ML	Fri Jul 14 16:32:44 2000 +0200
@@ -35,12 +35,10 @@
 
 Goalw [times_prod_def, one_prod_def] "1 * x = (x::'a::monoid*'b::monoid)";
 by (simp_tac (prod_ss addsimps [Monoid.left_unit]) 1);
-by (rtac (surjective_pairing RS sym) 1);
 qed "prod_left_unit";
 
 Goalw [times_prod_def, one_prod_def] "x * 1 = (x::'a::monoid*'b::monoid)";
 by (simp_tac (prod_ss addsimps [Monoid.right_unit]) 1);
-by (rtac (surjective_pairing RS sym) 1);
 qed "prod_right_unit";
 
 Goalw [times_prod_def, inverse_prod_def, one_prod_def]

--- a/src/HOL/MicroJava/J/JBasis.ML	Fri Jul 14 16:29:02 2000 +0200
+++ b/src/HOL/MicroJava/J/JBasis.ML	Fri Jul 14 16:32:44 2000 +0200
@@ -40,7 +40,6 @@
 val set_cs2 = set_cs delrules [ballE] addSEs [BallE];
 
 Addsimps [Let_def];
-Addsimps [surjective_pairing RS sym];
 
 (* To HOL.ML *)
 

--- 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);

--- a/src/HOL/UNITY/Extend.ML	Fri Jul 14 16:29:02 2000 +0200
+++ b/src/HOL/UNITY/Extend.ML	Fri Jul 14 16:32:44 2000 +0200
@@ -119,8 +119,7 @@
 AddDs [h_inject1];
 
 Goal "h(f z, g z) = z";
-by (simp_tac (simpset() addsimps [f_def, g_def, surjective_pairing RS sym,
-				  surj_h RS surj_f_inv_f]) 1);
+by (simp_tac (simpset() addsimps [f_def, g_def, surj_h RS surj_f_inv_f]) 1);
 qed "h_f_g_eq";