--- a/src/HOLCF/Cfun2.ML Tue Mar 25 10:43:01 1997 +0100
+++ b/src/HOLCF/Cfun2.ML Tue Mar 25 11:13:12 1997 +0100
@@ -41,7 +41,7 @@
bind_thm ("UU_cfun_def",minimal_cfun RS minimal2UU RS sym);
-qed_goal "least_cfun" thy "? x::'a->'b.!y.x<<y"
+qed_goal "least_cfun" thy "? x::'a->'b::pcpo.!y.x<<y"
(fn prems =>
[
(res_inst_tac [("x","fabs(% x.UU)")] exI 1),
@@ -237,7 +237,7 @@
*)
qed_goal "cpo_cfun" thy
- "is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x"
+ "is_chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x"
(fn prems =>
[
(cut_facts_tac prems 1),