diff -r cb82606b8215 -r 3fbcfa911863 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Tue Aug 13 15:59:22 2013 +0200
+++ b/src/HOL/Library/Mapping.thy	Tue Aug 13 15:59:22 2013 +0200
@@ -5,11 +5,15 @@
 header {* An abstract view on maps for code generation. *}
 
 theory Mapping
-imports Main Quotient_Option Quotient_List
+imports Main
 begin
 
 subsection {* Parametricity transfer rules *}
 
+context
+begin
+interpretation lifting_syntax .
+
 lemma empty_transfer: "(A ===> option_rel B) Map.empty Map.empty" by transfer_prover
 
 lemma lookup_transfer: "((A ===> B) ===> A ===> B) (\<lambda>m k. m k) (\<lambda>m k. m k)" by transfer_prover
@@ -72,6 +76,8 @@
       | Some v \<Rightarrow> m (k \<mapsto> (f v))))"
 by transfer_prover
 
+end
+
 subsection {* Type definition and primitive operations *}
 
 typedef ('a, 'b) mapping = "UNIV :: ('a \<rightharpoonup> 'b) set"
@@ -154,12 +160,17 @@
 
 end
 
+context
+begin
+interpretation lifting_syntax .
+
 lemma [transfer_rule]:
   assumes [transfer_rule]: "bi_total A"
   assumes [transfer_rule]: "bi_unique B"
-  shows  "fun_rel (pcr_mapping A B) (fun_rel (pcr_mapping A B) HOL.iff) HOL.eq HOL.equal"
+  shows  "(pcr_mapping A B ===> pcr_mapping A B ===> op=) HOL.eq HOL.equal"
 by (unfold equal) transfer_prover
 
+end
 
 subsection {* Properties *}