diff -r 76a96e32bd23 -r ae93953746fc 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>