--- a/src/HOL/Library/Mapping.thy Fri Mar 08 13:14:23 2013 +0100
+++ b/src/HOL/Library/Mapping.thy Fri Mar 08 13:21:06 2013 +0100
@@ -5,7 +5,7 @@
header {* An abstract view on maps for code generation. *}
theory Mapping
-imports Main Quotient_Option
+imports Main Quotient_Option Quotient_List
begin
subsection {* Type definition and primitive operations *}
@@ -81,7 +81,7 @@
end
lemma [transfer_rule]:
- "fun_rel cr_mapping (fun_rel cr_mapping HOL.iff) HOL.eq HOL.equal"
+ "fun_rel (pcr_mapping op= op=) (fun_rel (pcr_mapping op= op=) HOL.iff) HOL.eq HOL.equal"
by (unfold equal) transfer_prover