diff -r aa960d16570f -r b1f55dd64481 Quot/QuotList.thy
--- a/Quot/QuotList.thy	Thu Jan 21 12:50:43 2010 +0100
+++ b/Quot/QuotList.thy	Thu Jan 21 19:52:46 2010 +0100
@@ -74,7 +74,7 @@
 lemma cons_prs[quot_preserve]:
   assumes q: "Quotient R Abs Rep"
   shows "(Rep ---> (map Rep) ---> (map Abs)) (op #) = (op #)"
-by (simp only: expand_fun_eq fun_map.simps cons_prs_aux[OF q])
+by (simp only: expand_fun_eq fun_map_def cons_prs_aux[OF q])
    (simp)
 
 lemma cons_rsp[quot_respect]:
@@ -103,7 +103,7 @@
   assumes a: "Quotient R1 abs1 rep1"
   and     b: "Quotient R2 abs2 rep2"
   shows "((abs1 ---> rep2) ---> (map rep1) ---> (map abs2)) map = map"
-by (simp only: expand_fun_eq fun_map.simps map_prs_aux[OF a b])
+by (simp only: expand_fun_eq fun_map_def map_prs_aux[OF a b])
    (simp)
 
 
@@ -129,7 +129,7 @@
   assumes a: "Quotient R1 abs1 rep1"
   and     b: "Quotient R2 abs2 rep2"
   shows "((abs1 ---> abs2 ---> rep2) ---> (map rep1) ---> rep2 ---> abs2) foldr = foldr"
-by (simp only: expand_fun_eq fun_map.simps foldr_prs_aux[OF a b])
+by (simp only: expand_fun_eq fun_map_def foldr_prs_aux[OF a b])
    (simp)
 
 lemma foldl_prs_aux:
@@ -143,7 +143,7 @@
   assumes a: "Quotient R1 abs1 rep1"
   and     b: "Quotient R2 abs2 rep2"
   shows "((abs1 ---> abs2 ---> rep1) ---> rep1 ---> (map rep2) ---> abs1) foldl = foldl"
-by (simp only: expand_fun_eq fun_map.simps foldl_prs_aux[OF a b])
+by (simp only: expand_fun_eq fun_map_def foldl_prs_aux[OF a b])
    (simp)
 
 lemma list_rel_empty: "list_rel R [] b \<Longrightarrow> length b = 0"