--- a/src/HOLCF/Bifinite.thy Thu Oct 21 15:19:07 2010 -0700
+++ b/src/HOLCF/Bifinite.thy Thu Oct 21 15:21:39 2010 -0700
@@ -5,7 +5,7 @@
header {* Bifinite domains *}
theory Bifinite
-imports Algebraic Cprod Sprod Ssum Up Lift One Tr
+imports Algebraic Cprod Sprod Ssum Up Lift One Tr Countable
begin
subsection {* Class of bifinite domains *}
--- a/src/HOLCF/Lift.thy Thu Oct 21 15:19:07 2010 -0700
+++ b/src/HOLCF/Lift.thy Thu Oct 21 15:21:39 2010 -0700
@@ -5,7 +5,7 @@
header {* Lifting types of class type to flat pcpo's *}
theory Lift
-imports Discrete Up Countable
+imports Discrete Up
begin
default_sort type