
diff -r 49fa6aaa4529 -r fb5d8a50c641 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Tue Jun 21 17:35:45 2016 +0200
+++ b/src/HOL/Library/Mapping.thy	Wed Jun 22 10:09:20 2016 +0200
@@ -14,11 +14,9 @@
   "map_of xs = foldr (\<lambda>(k, v) m. m(k \<mapsto> v)) xs Map.empty"
   using map_add_map_of_foldr [of Map.empty] by auto
 
-context
+context includes lifting_syntax
 begin
 
-interpretation lifting_syntax .
-
 lemma empty_parametric:
   "(A ===> rel_option B) Map.empty Map.empty"
   by transfer_prover
@@ -219,11 +217,9 @@
 
 end
 
-context
+context includes lifting_syntax
 begin
 
-interpretation lifting_syntax .
-
 lemma [transfer_rule]:
   assumes [transfer_rule]: "bi_total A"
   assumes [transfer_rule]: "bi_unique B"




