src/HOL/Quotient_Examples/Lift_FSet.thy

--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Tue Jun 21 17:35:45 2016 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Wed Jun 22 10:09:20 2016 +0200
@@ -25,9 +25,8 @@
 lemma equivp_list_eq: "equivp list_eq"
   by (intro equivpI reflp_list_eq symp_list_eq transp_list_eq)
 
-context
+context includes lifting_syntax
 begin
-interpretation lifting_syntax .
 
 lemma list_eq_transfer [transfer_rule]:
   assumes [transfer_rule]: "bi_unique A"