src/HOL/Isar_examples/W_correct.thy

       proof (rule has_type.App);
         from s; have s': "$ u ($ s2 ($ s1 a)) = $s a";
           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);
           with s' t mgu_ok; show ?thesis; by simp;
         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);
           with s'; show ?thesis; by simp;
         qed;
       qed;
     };
   qed;
-  with W_ok [RS sym]; show ?thesis; by blast;
+  with W_ok [symmetric]; show ?thesis; by blast;
 qed;
 
 end;