src/HOL/HOLCF/Universal.thy

--- a/src/HOL/HOLCF/Universal.thy	Thu Dec 12 12:35:59 2024 +0100
+++ b/src/HOL/HOLCF/Universal.thy	Thu Dec 12 15:45:29 2024 +0100
@@ -255,7 +255,7 @@
 by (rule typedef_po)
 
 definition
-  approximants :: "'a \<Rightarrow> 'a compact_basis set" where
+  approximants :: "'a::pcpo \<Rightarrow> 'a compact_basis set" where
   "approximants = (\<lambda>x. {a. Rep_compact_basis a \<sqsubseteq> x})"
 
 definition