--- a/src/HOLCF/Fix.thy Tue Mar 23 12:20:27 2010 -0700
+++ b/src/HOLCF/Fix.thy Tue Mar 23 13:42:12 2010 -0700
@@ -6,7 +6,7 @@
header {* Fixed point operator and admissibility *}
theory Fix
-imports Cfun Cprod
+imports Cfun
begin
defaultsort pcpo
--- a/src/HOLCF/Fixrec.thy Tue Mar 23 12:20:27 2010 -0700
+++ b/src/HOLCF/Fixrec.thy Tue Mar 23 13:42:12 2010 -0700
@@ -5,7 +5,7 @@
header "Package for defining recursive functions in HOLCF"
theory Fixrec
-imports Sprod Ssum Up One Tr Fix
+imports Cprod Sprod Ssum Up One Tr Fix
uses
("Tools/holcf_library.ML")
("Tools/fixrec.ML")