src/HOL/HOLCF/Completion.thy

--- a/src/HOL/HOLCF/Completion.thy	Tue Apr 04 21:45:54 2017 +0200
+++ b/src/HOL/HOLCF/Completion.thy	Tue Apr 04 21:57:43 2017 +0200
@@ -5,7 +5,7 @@
 section \<open>Defining algebraic domains by ideal completion\<close>
 
 theory Completion
-imports Plain_HOLCF
+imports Cfun
 begin
 
 subsection \<open>Ideals over a preorder\<close>