# HG changeset patch
# User nipkow
# Date 781808998 -3600
# Node ID bb3f87f9cafea77390d4fe494ae41ab2b130ed7c
# Parent  e685b5411617eb83f1ae7e264afa0a0d937a5bfd
corrected problems with changed binding power of ::.

diff -r e685b5411617 -r bb3f87f9cafe src/HOLCF/Fix.ML
--- a/src/HOLCF/Fix.ML	Mon Oct 10 12:57:23 1994 +0100
+++ b/src/HOLCF/Fix.ML	Mon Oct 10 18:09:58 1994 +0100
@@ -693,17 +693,17 @@
 (* ------------------------------------------------------------------------- *)
 
 val flat_codom = prove_goalw Fix.thy [flat_def]
-"[|flat(y::'b);f[x::'a]=(c::'b)|] ==> f[UU::'a]=UU::'b | (!z.f[z::'a]=c)"
+"[|flat(y::'b);f[x::'a]=(c::'b)|] ==> f[UU::'a]=(UU::'b) | (!z.f[z::'a]=c)"
  (fn prems =>
 	[
 	(cut_facts_tac prems 1),
-	(res_inst_tac [("Q","f[x::'a]=UU::'b")] classical2 1),
+	(res_inst_tac [("Q","f[x::'a]=(UU::'b)")] classical2 1),
 	(rtac disjI1 1),
 	(rtac UU_I 1),
 	(res_inst_tac [("s","f[x]"),("t","UU::'b")] subst 1),
 	(atac 1),
 	(rtac (minimal RS monofun_cfun_arg) 1),
-	(res_inst_tac [("Q","f[UU::'a]=UU::'b")] classical2 1),
+	(res_inst_tac [("Q","f[UU::'a]=(UU::'b)")] classical2 1),
 	(etac disjI1 1),
 	(rtac disjI2 1),
 	(rtac allI 1),
diff -r e685b5411617 -r bb3f87f9cafe src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Mon Oct 10 12:57:23 1994 +0100
+++ b/src/HOLCF/Pcpo.thy	Mon Oct 10 18:09:58 1994 +0100
@@ -8,7 +8,7 @@
 rules
 
 minimal	"UU << x"	
-cpo	"is_chain(S) ==> ? x. range(S) <<| x::('a::pcpo)" 
+cpo	"is_chain(S) ==> ? x. range(S) <<| (x::'a::pcpo)" 
 
 inst_void_pcpo	"(UU::void) = UU_void"