diff -r 812ccc91bfa0 -r 3647161d15d3 src/HOLCF/Stream.ML
--- a/src/HOLCF/Stream.ML	Sat Mar 11 11:58:21 1995 +0100
+++ b/src/HOLCF/Stream.ML	Sat Mar 11 17:46:14 1995 +0100
@@ -141,7 +141,7 @@
 	]);
 
 val stream_constrdef = [
-	prover "is_scons[UU] ~= UU" "x~=UU ==> scons[x][xs]~=UU"
+	prover "is_scons[UU::'a stream] ~= UU" "x~=UU ==> scons[x::'a][xs]~=UU"
 	]; 
 
 fun prover defs thm = prove_goalw Stream.thy defs thm