# HG changeset patch
# User paulson
# Date 927553784 -7200
# Node ID d45359e7dcbf137a86862615c163c77482a8e7e7
# Parent  4d438b71457175f9fb4d8f05b92c067fc725aeab
updated for stronger version of psp

diff -r 4d438b714571 -r d45359e7dcbf src/HOL/UNITY/Token.ML
--- a/src/HOL/UNITY/Token.ML	Mon May 24 15:49:24 1999 +0200
+++ b/src/HOL/UNITY/Token.ML	Mon May 24 15:49:44 1999 +0200
@@ -108,7 +108,7 @@
 Goal "j<N ==> F : ({s. token s < N} Int H j) leadsTo (E j)";
 by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1);
 by (rtac TR6 2);
-by (rtac leadsTo_weaken_R 1);
+by (rtac leadsTo_weaken 1);
 by (rtac ([leadsTo_j, TR3] MRS psp) 1);
 by (ALLGOALS Blast_tac);
 qed "token_progress";