src/HOLCF/HOLCF.thy

--- a/src/HOLCF/HOLCF.thy	Mon Jan 14 19:26:01 2008 +0100
+++ b/src/HOLCF/HOLCF.thy	Mon Jan 14 19:26:41 2008 +0100
@@ -6,7 +6,7 @@
 *)
 
 theory HOLCF
-imports Sprod Ssum Up Lift Discrete One Tr Domain Main
+imports Sprod Ssum Up Lift Discrete One Tr Domain ConvexPD Main
 uses
   "holcf_logic.ML"
   "Tools/cont_consts.ML"
@@ -19,6 +19,8 @@
 
 begin
 
+defaultsort pcpo
+
 ML_setup {*
   change_simpset (fn simpset => simpset addSolver
     (mk_solver' "adm_tac" (fn ss =>