--- a/src/HOLCF/IOA/meta_theory/CompoTraces.ML Thu Oct 30 14:17:33 1997 +0100
+++ b/src/HOLCF/IOA/meta_theory/CompoTraces.ML Thu Oct 30 14:18:14 1997 +0100
@@ -699,7 +699,7 @@
\ --> Filter (%a. a:act A)`(mksch A B`tr`schA`schB) = schA";
by (strip_tac 1);
-by (rtac seq.take_lemma 1);
+by (resolve_tac seq.take_lemmas 1);
by (rtac mp 1);
by (assume_tac 2);
back();back();back();back();
@@ -941,7 +941,7 @@
\ --> Filter (%a. a:act B)`(mksch A B`tr`schA`schB) = schB";
by (strip_tac 1);
-by (rtac seq.take_lemma 1);
+by (resolve_tac seq.take_lemmas 1);
by (rtac mp 1);
by (assume_tac 2);
back();back();back();back();