--- a/src/HOLCF/ex/Stream.ML Wed Dec 12 19:22:21 2001 +0100
+++ b/src/HOLCF/ex/Stream.ML Wed Dec 12 20:37:31 2001 +0100
@@ -28,7 +28,7 @@
qed "scons_eq_UU";
Goal "[| a && x = UU; a ~= UU |] ==> R";
-by (dresolve_tac [stream_con_rew2] 1);
+by (dtac stream_con_rew2 1);
by (contr_tac 1);
qed "scons_not_empty";
@@ -534,7 +534,7 @@
\!s. #(s::'a::flat stream) = #t & s << t --> s = t";
by (etac stream_finite_ind 1);
by (fast_tac (claset() addDs [eq_UU_iff RS iffD2]) 1);
-by (Safe_tac);
+by Safe_tac;
by (stream_case_tac "sa" 1);
by (dtac sym 1);
by (Asm_full_simp_tac 1);