diff -r 290c4dfc34ba -r 3eb91524b938 src/HOL/Relation.ML
--- a/src/HOL/Relation.ML	Wed Oct 04 13:01:05 1995 +0100
+++ b/src/HOL/Relation.ML	Wed Oct 04 13:10:03 1995 +0100
@@ -83,7 +83,7 @@
 (** Natural deduction for converse(r) **)
 
 goalw Relation.thy [converse_def] "!!a b r. (a,b):r ==> (b,a):converse(r)";
-by (simp_tac prod_ss 1);
+by (Simp_tac 1);
 by (fast_tac set_cs 1);
 qed "converseI";
 
@@ -170,4 +170,4 @@
 
 val rel_eq_cs = rel_cs addSIs [equalityI];
 
-val rel_ss = prod_ss addsimps [pair_in_id_conv];
+Addsimps [pair_in_id_conv];