diff -r 6125cc9efc18 -r 1adf6d761c97 src/HOL/Isar_examples/W_correct.thy
--- a/src/HOL/Isar_examples/W_correct.thy	Thu Aug 17 10:33:37 2000 +0200
+++ b/src/HOL/Isar_examples/W_correct.thy	Thu Aug 17 10:34:11 2000 +0200
@@ -126,7 +126,7 @@
           by (simp add: subst_comp_tel o_def);
         show "$s a |- e1 :: $ u t2 -> t";
         proof -;
-          from hyp1 W1_ok [RS sym]; have "$ s1 a |- e1 :: t1";
+          from hyp1 W1_ok [symmetric]; have "$ s1 a |- e1 :: t1";
             by blast;
           hence "$ u ($ s2 ($ s1 a)) |- e1 :: $ u ($ s2 t1)";
             by (intro has_type_subst_closed);
@@ -134,7 +134,7 @@
         qed;
         show "$ s a |- e2 :: $ u t2";
         proof -;
-          from hyp2 W2_ok [RS sym];
+          from hyp2 W2_ok [symmetric];
           have "$ s2 ($ s1 a) |- e2 :: t2"; by blast;
           hence "$ u ($ s2 ($ s1 a)) |- e2 :: $ u t2";
             by (rule has_type_subst_closed);
@@ -143,7 +143,7 @@
       qed;
     };
   qed;
-  with W_ok [RS sym]; show ?thesis; by blast;
+  with W_ok [symmetric]; show ?thesis; by blast;
 qed;
 
 end;