src/HOLCF/Cfun2.ML
changeset 2838 2e908f29bc3d
parent 2640 ee4dfce170a0
child 3323 194ae2e0c193
--- 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),