
diff -r 7e03e61612b0 -r c2508f4ab739 src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Wed Mar 26 13:44:05 1997 +0100
+++ b/src/HOLCF/Fix.thy	Wed Mar 26 17:58:48 1997 +0100
@@ -15,10 +15,10 @@
 iterate	:: "nat=>('a->'a)=>'a=>'a"
 Ifix	:: "('a->'a)=>'a"
 fix	:: "('a->'a)->'a"
-adm		:: "('a=>bool)=>bool"
+adm		:: "('a::cpo=>bool)=>bool"
 admw		:: "('a=>bool)=>bool"
-chain_finite	:: "'a=>bool"
-flat		:: "'a=>bool" (* should be called flat, for consistency *)
+chain_finite	:: "'a::cpo=>bool"
+flat		:: "'a=>bool"
 
 defs
 
@@ -32,8 +32,8 @@
 admw_def      "admw P == !F. (!n.P (iterate n F UU)) -->
                             P (lub(range (%i. iterate i F UU)))" 
 
-chain_finite_def  "chain_finite (x::'a)==
-                        !Y. is_chain (Y::nat=>'a) --> (? n.max_in_chain n Y)"
+chain_finite_def  "chain_finite (x::'a::cpo)==
+                   !Y. is_chain (Y::nat=>'a::cpo) --> (? n.max_in_chain n Y)"
 
 flat_def	  "flat (x::'a) == ! x y. (x::'a) << y --> (x = UU) | (x=y)"
 




