--- a/src/HOL/Filter.thy Tue Jun 21 17:35:45 2016 +0200
+++ b/src/HOL/Filter.thy Wed Jun 22 10:09:20 2016 +0200
@@ -1192,7 +1192,8 @@
subsection \<open>Setup @{typ "'a filter"} for lifting and transfer\<close>
-context begin interpretation lifting_syntax .
+context includes lifting_syntax
+begin
definition rel_filter :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a filter \<Rightarrow> 'b filter \<Rightarrow> bool"
where "rel_filter R F G = ((R ===> op =) ===> op =) (Rep_filter F) (Rep_filter G)"