# HG changeset patch
# User haftmann
# Date 1330119976 -3600
# Node ID 7fe029e818c260a2a93cb5f042cf816789797e18
# Parent  4e258158be3882f145bb3c1f6b8ca71679c3d970
explicit is better than implicit

diff -r 4e258158be38 -r 7fe029e818c2 src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Fri Feb 24 18:46:01 2012 +0100
+++ b/src/HOL/Library/Quotient_List.thy	Fri Feb 24 22:46:16 2012 +0100
@@ -12,7 +12,7 @@
 
 lemma map_id [id_simps]:
   "map id = id"
-  by (fact map.id)
+  by (fact List.map.id)
 
 lemma list_all2_eq [id_simps]:
   "list_all2 (op =) = (op =)"
diff -r 4e258158be38 -r 7fe029e818c2 src/HOL/Quotient_Examples/FSet.thy
--- a/src/HOL/Quotient_Examples/FSet.thy	Fri Feb 24 18:46:01 2012 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy	Fri Feb 24 22:46:16 2012 +0100
@@ -125,7 +125,7 @@
 proof (intro conjI allI)
   fix a r s
   show "abs_fset (map Abs (map Rep (rep_fset a))) = a"
-    by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] map.id)
+    by (simp add: abs_o_rep[OF q] Quotient_abs_rep[OF Quotient_fset] List.map.id)
   have b: "list_all2 R (map Rep (rep_fset a)) (map Rep (rep_fset a))"
     by (rule list_all2_refl'[OF e])
   have c: "(op \<approx> OO list_all2 R) (map Rep (rep_fset a)) (map Rep (rep_fset a))"
@@ -500,7 +500,7 @@
   and     r: "Quotient R2 Abs2 Rep2"
   shows "((map Rep1 \<circ> Rep2) ---> (map Rep1 \<circ> Rep2) ---> (Abs2 \<circ> map Abs1)) op @ =
     (Rep2 ---> Rep2 ---> Abs2) op @"
-  by (simp add: fun_eq_iff abs_o_rep[OF q] map.id)
+  by (simp add: fun_eq_iff abs_o_rep[OF q] List.map.id)
 
 lemma list_all2_app_l:
   assumes a: "reflp R"