src/HOL/Lifting_Set.thy

--- a/src/HOL/Lifting_Set.thy	Tue Jun 21 17:35:45 2016 +0200
+++ b/src/HOL/Lifting_Set.thy	Wed Jun 22 10:09:20 2016 +0200
@@ -112,11 +112,9 @@
 
 subsubsection \<open>Unconditional transfer rules\<close>
 
-context
+context includes lifting_syntax
 begin
 
-interpretation lifting_syntax .
-
 lemma empty_transfer [transfer_rule]: "(rel_set A) {} {}"
   unfolding rel_set_def by simp