diff -r 88ff48884d26 -r 8fb6cc6f3b94 src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Tue Apr 20 14:56:20 2010 +0200
+++ b/src/HOL/Library/Quotient_List.thy	Tue Apr 20 14:56:58 2010 +0200
@@ -130,24 +130,24 @@
   by (induct l)
      (simp_all add: Quotient_abs_rep[OF a] Quotient_abs_rep[OF b])
 
-
 lemma map_prs[quot_preserve]:
   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_def map_prs_aux[OF a b])
-     (simp)
-
+  and   "((abs1 ---> id) ---> map rep1 ---> id) map = map"
+  by (simp_all only: expand_fun_eq fun_map_def map_prs_aux[OF a b])
+     (simp_all add: Quotient_abs_rep[OF a])
 
 lemma map_rsp[quot_respect]:
   assumes q1: "Quotient R1 Abs1 Rep1"
   and     q2: "Quotient R2 Abs2 Rep2"
   shows "((R1 ===> R2) ===> (list_rel R1) ===> list_rel R2) map map"
-  apply(simp)
-  apply(rule allI)+
-  apply(rule impI)
-  apply(rule allI)+
-  apply (induct_tac xa ya rule: list_induct2')
+  and   "((R1 ===> op =) ===> (list_rel R1) ===> op =) map map"
+  apply simp_all
+  apply(rule_tac [!] allI)+
+  apply(rule_tac [!] impI)
+  apply(rule_tac [!] allI)+
+  apply (induct_tac [!] xa ya rule: list_induct2')
   apply simp_all
   done