--- 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),