# HG changeset patch
# User nipkow
# Date 794940374 -3600
# Node ID 3647161d15d3a18d6cb404d55bac2f678ca030c4
# Parent  812ccc91bfa0babf50e7c311fb489d7a23360c9b
Added type constraints to enforce correct choice of variable names.

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