# HG changeset patch
# User nipkow
# Date 757795426 -3600
# Node ID 4a10bc05210a72f8903c3381f774df7ba3a075d4
# Parent  bc439e9ce95866ad24ab7795a43de8187a2b79e9
adapted a proof to the new solver (see change of FOL/simpdata.ML)

diff -r bc439e9ce958 -r 4a10bc05210a src/CCL/ex/Stream.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);
diff -r bc439e9ce958 -r 4a10bc05210a src/CCL/ex/stream.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);