Added type constraints to enforce correct choice of variable names.
authornipkow
Sat, 11 Mar 1995 17:46:14 +0100
changeset 948 3647161d15d3
parent 947 812ccc91bfa0
child 949 83c588d6fee9
Added type constraints to enforce correct choice of variable names.
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