src/HOL/UNITY/Mutex.ML

 by (rtac LeadsTo_cancel2 1);
 by (rtac U_F2 2);
 by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
 by (stac Un_commute 1);
 by (rtac LeadsTo_Un_duplicate 1);
-by (rtac ([v_leadsto_not_p, U_F0] MRS R_PSP_unless RSN(2, LeadsTo_cancel2)) 1);
+by (rtac ([v_leadsto_not_p, U_F0] MRS PSP_unless RSN(2, LeadsTo_cancel2)) 1);
 by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
 by (auto_tac (claset() addSEs [less_SucE], simpset()));
 qed "m1_leadsto_3";
 
 

 by (rtac LeadsTo_cancel2 1);
 by (rtac V_F2 2);
 by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
 by (stac Un_commute 1);
 by (rtac LeadsTo_Un_duplicate 1);
-by (rtac ([u_leadsto_p, V_F0] MRS R_PSP_unless  RSN(2, LeadsTo_cancel2)) 1);
+by (rtac ([u_leadsto_p, V_F0] MRS PSP_unless  RSN(2, LeadsTo_cancel2)) 1);
 by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
 by (auto_tac (claset() addSEs [less_SucE], simpset()));
 qed "n1_leadsto_3";