# HG changeset patch
# User lcp
# Date 783682338 -3600
# Node ID f304c8379e4d736a141cb7cedc25b8caf4b8ad8e
# Parent  59a4fa76b5909494d11ae2d9dd2d225eafdd0e5c
HOLCF/Ssum3.ML: changed res_inst_tac [("P"... to res_inst_tac [("Pa" in
some very ugly proofs.  Needed to handle new variable names in swap.

diff -r 59a4fa76b590 -r f304c8379e4d src/HOLCF/Ssum3.ML
--- a/src/HOLCF/Ssum3.ML	Mon Oct 31 18:15:24 1994 +0100
+++ b/src/HOLCF/Ssum3.ML	Tue Nov 01 10:32:18 1994 +0100
@@ -242,14 +242,14 @@
 	(rtac trans 1),
 	(rtac cfun_arg_cong 1),
 	(rtac Iwhen2 1),
-	(res_inst_tac [("P","Y(i)=UU")] swap 1),
+	(res_inst_tac [("Pa","Y(i)=UU")] swap 1),
 	(fast_tac HOL_cs 1),
 	(rtac (inst_ssum_pcpo RS ssubst) 1),
 	(res_inst_tac [("t","Y(i)")] ssubst 1),
 	(atac 1),
 	(fast_tac HOL_cs 1),
 	(rtac (Iwhen2 RS ssubst) 1),
-	(res_inst_tac [("P","Y(i)=UU")] swap 1),
+	(res_inst_tac [("Pa","Y(i)=UU")] swap 1),
 	(fast_tac HOL_cs 1),
 	(rtac (inst_ssum_pcpo RS ssubst) 1),
 	(res_inst_tac [("t","Y(i)")] ssubst 1),
@@ -302,7 +302,7 @@
 	(rtac trans 1),
 	(rtac cfun_arg_cong 1),
 	(rtac Iwhen3 1),
-	(res_inst_tac [("P","Y(i)=UU")] swap 1),
+	(res_inst_tac [("Pa","Y(i)=UU")] swap 1),
 	(fast_tac HOL_cs 1),
 	(dtac notnotD 1),
 	(rtac (inst_ssum_pcpo RS ssubst) 1),
@@ -311,7 +311,7 @@
 	(atac 1),
 	(fast_tac HOL_cs 1),
 	(rtac (Iwhen3 RS ssubst) 1),
-	(res_inst_tac [("P","Y(i)=UU")] swap 1),
+	(res_inst_tac [("Pa","Y(i)=UU")] swap 1),
 	(fast_tac HOL_cs 1),
 	(dtac notnotD 1),
 	(rtac (inst_ssum_pcpo RS ssubst) 1),