diff -r 07f4bf913230 -r b75ce48a93ee src/HOL/Quotient.thy
--- a/src/HOL/Quotient.thy	Tue Apr 03 17:26:30 2012 +0900
+++ b/src/HOL/Quotient.thy	Tue Apr 03 17:45:06 2012 +0900
@@ -717,9 +717,9 @@
 apply (rule QuotientI)
    apply (simp add: o_def Quotient_abs_rep [OF R2] Quotient_abs_rep [OF R1])
   apply simp
-  apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI)
+  apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI)
    apply (rule Quotient_rep_reflp [OF R1])
-  apply (rule_tac b="Rep1 (Rep2 a)" in pred_compI [rotated])
+  apply (rule_tac b="Rep1 (Rep2 a)" in relcomppI [rotated])
    apply (rule Quotient_rep_reflp [OF R1])
   apply (rule Rep1)
   apply (rule Quotient_rep_reflp [OF R2])
@@ -730,8 +730,8 @@
      apply (erule Quotient_refl1 [OF R1])
     apply (drule Quotient_refl1 [OF R2], drule Rep1)
     apply (subgoal_tac "R1 r (Rep1 (Abs1 x))")
-     apply (rule_tac b="Rep1 (Abs1 x)" in pred_compI, assumption)
-     apply (erule pred_compI)
+     apply (rule_tac b="Rep1 (Abs1 x)" in relcomppI, assumption)
+     apply (erule relcomppI)
      apply (erule Quotient_symp [OF R1, THEN sympD])
     apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
     apply (rule conjI, erule Quotient_refl1 [OF R1])
@@ -744,8 +744,8 @@
     apply (erule Quotient_refl1 [OF R1])
    apply (drule Quotient_refl2 [OF R2], drule Rep1)
    apply (subgoal_tac "R1 s (Rep1 (Abs1 y))")
-    apply (rule_tac b="Rep1 (Abs1 y)" in pred_compI, assumption)
-    apply (erule pred_compI)
+    apply (rule_tac b="Rep1 (Abs1 y)" in relcomppI, assumption)
+    apply (erule relcomppI)
     apply (erule Quotient_symp [OF R1, THEN sympD])
    apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
    apply (rule conjI, erule Quotient_refl2 [OF R1])
@@ -761,11 +761,11 @@
   apply (erule Quotient_refl1 [OF R1])
  apply (rename_tac a b c d)
  apply simp
- apply (rule_tac b="Rep1 (Abs1 r)" in pred_compI)
+ apply (rule_tac b="Rep1 (Abs1 r)" in relcomppI)
   apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
   apply (rule conjI, erule Quotient_refl1 [OF R1])
   apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
- apply (rule_tac b="Rep1 (Abs1 s)" in pred_compI [rotated])
+ apply (rule_tac b="Rep1 (Abs1 s)" in relcomppI [rotated])
   apply (rule Quotient_rel[symmetric, OF R1, THEN iffD2])
   apply (simp add: Quotient_abs_rep [OF R1] Quotient_rep_reflp [OF R1])
   apply (erule Quotient_refl2 [OF R1])