--- a/src/HOLCF/explicit_domains/Dnat.ML Thu Sep 26 12:50:48 1996 +0200
+++ b/src/HOLCF/explicit_domains/Dnat.ML Thu Sep 26 15:14:23 1996 +0200
@@ -339,10 +339,10 @@
[
(res_inst_tac [("t","s1")] (reach RS subst) 1),
(res_inst_tac [("t","s2")] (reach RS subst) 1),
- (rtac (fix_def2 RS ssubst) 1),
- (rtac (contlub_cfun_fun RS ssubst) 1),
+ (stac fix_def2 1),
+ (stac contlub_cfun_fun 1),
(rtac is_chain_iterate 1),
- (rtac (contlub_cfun_fun RS ssubst) 1),
+ (stac contlub_cfun_fun 1),
(rtac is_chain_iterate 1),
(rtac lub_equal 1),
(rtac (is_chain_iterate RS ch2ch_fappL) 1),