# HG changeset patch
# User paulson
# Date 927553496 -7200
# Node ID 27a2e763daf8f1bcc7a725cf77b2c67963506565
# Parent  e84a0b941beb925f2f9ef980c10bce544099d47e
renamed PSP_stable2->PSP_Stable2

diff -r e84a0b941beb -r 27a2e763daf8 src/HOL/UNITY/Common.ML
--- a/src/HOL/UNITY/Common.ML	Mon May 24 15:44:20 1999 +0200
+++ b/src/HOL/UNITY/Common.ML	Mon May 24 15:44:56 1999 +0200
@@ -76,7 +76,7 @@
 by (res_inst_tac [("f","%x. x"), ("l", "n")] GreaterThan_bounded_induct 1);
 by (ALLGOALS Asm_simp_tac);
 by (rtac subset_refl 2);
-by (blast_tac (claset() addDs [PSP_stable2] 
+by (blast_tac (claset() addDs [PSP_Stable2] 
                         addIs [common_stable, LeadsTo_weaken_R]) 1);
 val lemma = result();