adapted a proof to the new solver (see change of FOL/simpdata.ML)

--- a/src/CCL/ex/Stream.ML	Wed Jan 05 19:41:37 1994 +0100
+++ b/src/CCL/ex/Stream.ML	Wed Jan 05 19:43:46 1994 +0100
@@ -108,7 +108,6 @@
 by (fast_tac (type_cs addSIs [napplyBzero RS sym,
 			      napplyBzero RS sym RS arg_cong]) 1);
 by (EQgen_tac list_ss [iter1B,iter2Blemma] 1);
-by (assume_tac 1);   (*should EQgen_tac call asm_simp_tac?*)
 by (rtac (napply_f RS ssubst) 1 THEN atac 1);
 by (res_inst_tac [("f1","f")] (napplyBsucc RS subst) 1);
 by (fast_tac type_cs 1);

--- a/src/CCL/ex/stream.ML	Wed Jan 05 19:41:37 1994 +0100
+++ b/src/CCL/ex/stream.ML	Wed Jan 05 19:43:46 1994 +0100
@@ -108,7 +108,6 @@
 by (fast_tac (type_cs addSIs [napplyBzero RS sym,
 			      napplyBzero RS sym RS arg_cong]) 1);
 by (EQgen_tac list_ss [iter1B,iter2Blemma] 1);
-by (assume_tac 1);   (*should EQgen_tac call asm_simp_tac?*)
 by (rtac (napply_f RS ssubst) 1 THEN atac 1);
 by (res_inst_tac [("f1","f")] (napplyBsucc RS subst) 1);
 by (fast_tac type_cs 1);