src/HOLCF/Fix.ML

 	fast_tac ((HOL_cs addSIs [flatdom2monofun,
 			flat_imp_chain_finite RS chfindom_monofun2cont])) 1
 	]);
 
 qed_goal "chfin_fappR" thy 
-    "[| is_chain (Y::nat => 'a->'b); chain_finite(x::'b) |] ==> \
+    "[| is_chain (Y::nat => 'a::cpo->'b); chain_finite(x::'b) |] ==> \
 \    !s. ? n. lub(range(Y))`s = Y n`s" 
 (fn prems => 
 	[
 	cut_facts_tac prems 1,
 	rtac allI 1,

 	 atac 1,
 	fast_tac (HOL_cs addSIs [thelubI,lub_finch2,chfin2finch,ch2ch_fappL])1
 	]);
 
 qed_goalw "adm_chfindom" thy [adm_def]
-	    "chain_finite (x::'b) ==> adm (%(u::'a->'b). P(u`s))" (fn prems => [
+    "chain_finite (x::'b) ==> adm (%(u::'a::cpo->'b). P(u`s))"
+    (fn prems => [
 	cut_facts_tac prems 1,
 	strip_tac 1,
 	dtac chfin_fappR 1,
 	 atac 1,
 	eres_inst_tac [("x","s")] allE 1,

         etac mp 1,
         trans_tac 1
         ]);
 
   val adm_disj_lemma5 = prove_goal thy
-  "!!Y::nat=>'a. [| is_chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\
+  "!!Y::nat=>'a::cpo. [| is_chain(Y); ! j. i < j --> Q(Y(j)) |] ==>\
   \       lub(range(Y)) = lub(range(%m. if m< Suc(i) then Y(Suc(i)) else Y m))"
  (fn prems =>
         [
         safe_tac (HOL_cs addSIs [lub_equal2,adm_disj_lemma3]),
         atac 2,

         strip_tac 1,
         trans_tac 1
         ]);
 
   val adm_disj_lemma6 = prove_goal thy
-  "[| is_chain(Y::nat=>'a); ? i. ! j. i < j --> Q(Y(j)) |] ==>\
+  "[| is_chain(Y::nat=>'a::cpo); ? i. ! j. i < j --> Q(Y(j)) |] ==>\
   \         ? X. is_chain(X) & (! n. Q(X(n))) & lub(range(Y)) = lub(range(X))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (etac exE 1),

         (atac 1),
         (atac 1)
         ]);
 
   val adm_disj_lemma7 = prove_goal thy 
-  "[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j))  |] ==>\
+  "[| is_chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j))  |] ==>\
   \         is_chain(%m. Y(Least(%j. m<j & P(Y(j)))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (rtac is_chainI 1),

         (etac exE 1),
         (etac (LeastI RS conjunct2) 1)
         ]);
 
   val adm_disj_lemma9 = prove_goal thy
-  "[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
+  "[| is_chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==>\
   \         lub(range(Y)) = lub(range(%m. Y(Least(%j. m<j & P(Y(j))))))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (rtac antisym_less 1),

         (atac 1),
         (rtac lessI 1)
         ]);
 
   val adm_disj_lemma10 = prove_goal thy
-  "[| is_chain(Y::nat=>'a); ! i. ? j. i < j & P(Y(j)) |] ==>\
+  "[| is_chain(Y::nat=>'a::cpo); ! i. ? j. i < j & P(Y(j)) |] ==>\
   \         ? X. is_chain(X) & (! n. P(X(n))) & lub(range(Y)) = lub(range(X))"
  (fn prems =>
         [
         (cut_facts_tac prems 1),
         (res_inst_tac [("x","%m. Y(Least(%j. m<j & P(Y(j))))")] exI 1),