--- a/src/HOL/Algebra/Complete_Lattice.thy Thu Jan 04 18:18:57 2018 +0100
+++ b/src/HOL/Algebra/Complete_Lattice.thy Fri Jan 05 15:24:57 2018 +0100
@@ -1171,7 +1171,7 @@
subsubsection \<open>The Powerset of a Set is a Complete Lattice\<close>
theorem powerset_is_complete_lattice:
- "complete_lattice \<lparr>carrier = Pow A, eq = op =, le = op \<subseteq>\<rparr>"
+ "complete_lattice \<lparr>carrier = Pow A, eq = op =, le = (op \<subseteq>)\<rparr>"
(is "complete_lattice ?L")
proof (rule partial_order.complete_latticeI)
show "partial_order ?L"