1.1 --- a/src/HOLCF/Cfun2.ML	Tue Mar 25 10:43:01 1997 +0100
     1.2 +++ b/src/HOLCF/Cfun2.ML	Tue Mar 25 11:13:12 1997 +0100
     1.3 @@ -41,7 +41,7 @@
     1.4  
     1.5  bind_thm ("UU_cfun_def",minimal_cfun RS minimal2UU RS sym);
     1.6  
     1.7 -qed_goal "least_cfun" thy "? x::'a->'b.!y.x<<y"
     1.8 +qed_goal "least_cfun" thy "? x::'a->'b::pcpo.!y.x<<y"
     1.9  (fn prems =>
    1.10          [
    1.11          (res_inst_tac [("x","fabs(% x.UU)")] exI 1),
    1.12 @@ -237,7 +237,7 @@
    1.13  *)
    1.14  
    1.15  qed_goal "cpo_cfun" thy 
    1.16 -  "is_chain(CCF::nat=>('a::pcpo->'b::pcpo)) ==> ? x. range(CCF) <<| x"
    1.17 +  "is_chain(CCF::nat=>('a->'b)) ==> ? x. range(CCF) <<| x"
    1.18  (fn prems =>
    1.19          [
    1.20          (cut_facts_tac prems 1),