diff -r dee1c7f1f576 -r 2e908f29bc3d src/HOLCF/Fun2.ML
--- a/src/HOLCF/Fun2.ML	Tue Mar 25 10:43:01 1997 +0100
+++ b/src/HOLCF/Fun2.ML	Tue Mar 25 11:13:12 1997 +0100
@@ -86,7 +86,7 @@
 (* ------------------------------------------------------------------------ *)
 
 qed_goal "lub_fun"  Fun2.thy
-        "is_chain(S::nat=>('a::term => 'b::pcpo)) ==> \
+        "is_chain(S::nat=>('a::term => 'b::cpo)) ==> \
 \        range(S) <<| (% x.lub(range(% i.S(i)(x))))"
 (fn prems =>
         [
@@ -111,7 +111,7 @@
 (* is_chain ?S1 ==> lub (range ?S1) = (%x. lub (range (%i. ?S1 i x))) *)
 
 qed_goal "cpo_fun"  Fun2.thy
-        "is_chain(S::nat=>('a::term => 'b::pcpo)) ==> ? x. range(S) <<| x"
+        "is_chain(S::nat=>('a::term => 'b::cpo)) ==> ? x. range(S) <<| x"
 (fn prems =>
         [
         (cut_facts_tac prems 1),