diff -r 5e59af604d4f -r 8161f137b0e9 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 =>