diff -r d75a28a13639 -r e090bdb4e1c5 src/HOL/Library/Quotient_List.thy
--- a/src/HOL/Library/Quotient_List.thy	Mon May 10 14:53:33 2010 -0700
+++ b/src/HOL/Library/Quotient_List.thy	Tue May 11 07:45:47 2010 +0100
@@ -52,12 +52,17 @@
 lemma list_rel_transp:
   assumes a: "equivp R"
   shows "list_rel R xs1 xs2 \<Longrightarrow> list_rel R xs2 xs3 \<Longrightarrow> list_rel R xs1 xs3"
-  apply(induct xs1 xs2 arbitrary: xs3 rule: list_induct2')
-  apply(simp_all)
+  using a
+  apply(induct R xs1 xs2 arbitrary: xs3 rule: list_rel.induct)
+  apply(simp)
+  apply(simp)
+  apply(simp)
   apply(case_tac xs3)
-  apply(simp_all)
-  apply(rule equivp_transp[OF a])
-  apply(auto)
+  apply(clarify)
+  apply(simp (no_asm_use))
+  apply(clarify)
+  apply(simp (no_asm_use))
+  apply(auto intro: equivp_transp)
   done
 
 lemma list_equivp[quot_equiv]: