diff -r a9b20bc32fa6 -r ead56ad40e15 src/HOL/Library/Combine_PER.thy
--- a/src/HOL/Library/Combine_PER.thy	Mon Sep 20 23:15:02 2021 +0200
+++ b/src/HOL/Library/Combine_PER.thy	Tue Sep 21 00:20:47 2021 +0200
@@ -3,9 +3,11 @@
 section \<open>A combinator to build partial equivalence relations from a predicate and an equivalence relation\<close>
 
 theory Combine_PER
-  imports Main Lattice_Syntax
+  imports Main
 begin
 
+unbundle lattice_syntax
+
 definition combine_per :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"
   where "combine_per P R = (\<lambda>x y. P x \<and> P y) \<sqinter> R"