Repaired a proof that did, after all, refer to the theorem nat_induct2.

--- a/src/HOLCF/ex/Stream.thy	Tue Feb 10 09:58:58 2009 +0000
+++ b/src/HOLCF/ex/Stream.thy	Tue Feb 10 10:25:09 2009 +0000
@@ -252,7 +252,9 @@
 lemma stream_finite_ind2:
 "[| P UU; !! x. x ~= UU ==> P (x && UU); !! y z s. [| y ~= UU; z ~= UU; P s |] ==> P (y && z && s )|] ==>
                                  !s. P (stream_take n$s)"
-apply (rule nat_induct2 [of _ n],auto)
+apply (rule nat_less_induct [of _ n],auto)
+apply (case_tac n, auto) 
+apply (case_tac nat, auto) 
 apply (case_tac "s=UU",clarsimp)
 apply (drule stream_exhaust_eq [THEN iffD1],clarsimp)
 apply (case_tac "s=UU",clarsimp)