# HG changeset patch
# User kuncar
# Date 1350662056 -7200
# Node ID eb8b434158c88137a8df5d873d4a059ba7276de5
# Parent  463cdbfba8c73882c2f8dfc2ac53a0763d50922c
don't include Quotient_Option - workaround to a transfer bug

diff -r 463cdbfba8c7 -r eb8b434158c8 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Fri Oct 19 20:15:14 2012 +0200
+++ b/src/HOL/Library/Mapping.thy	Fri Oct 19 17:54:16 2012 +0200
@@ -5,7 +5,7 @@
 header {* An abstract view on maps for code generation. *}
 
 theory Mapping
-imports Main "~~/src/HOL/Library/Quotient_Option"
+imports Main
 begin
 
 subsection {* Type definition and primitive operations *}
@@ -61,7 +61,10 @@
     | Some v \<Rightarrow> m (k \<mapsto> (f v)))" .
 
 lemma map_entry_code [code]: "map_entry k f m = (case lookup m k of None \<Rightarrow> m
-    | Some v \<Rightarrow> update k (f v) m)" by transfer rule
+    | Some v \<Rightarrow> update k (f v) m)" 
+    apply (cases "lookup m k") 
+    apply simp_all 
+    by (transfer, simp)+
 
 definition map_default :: "'a \<Rightarrow> 'b \<Rightarrow> ('b \<Rightarrow> 'b) \<Rightarrow> ('a, 'b) mapping \<Rightarrow> ('a, 'b) mapping" where
   "map_default k v f m = map_entry k f (default k v m)" 
diff -r 463cdbfba8c7 -r eb8b434158c8 src/HOL/Library/RBT.thy
--- a/src/HOL/Library/RBT.thy	Fri Oct 19 20:15:14 2012 +0200
+++ b/src/HOL/Library/RBT.thy	Fri Oct 19 17:54:16 2012 +0200
@@ -97,9 +97,6 @@
   "RBT_Impl.keys (impl_of t) = keys t"
   by transfer (rule refl)
 
-(* FIXME *)
-lemma [transfer_rule]: "(fun_rel (fun_rel op = op =) op =) dom dom" unfolding fun_rel_def by auto
-
 lemma lookup_keys: 
   "dom (lookup t) = set (keys t)" 
   by transfer (simp add: rbt_lookup_keys)