src/HOL/Rat.thy

--- a/src/HOL/Rat.thy	Mon Nov 29 13:44:54 2010 +0100
+++ b/src/HOL/Rat.thy	Mon Nov 29 22:32:06 2010 +0100
@@ -781,7 +781,7 @@
 
 lemma of_rat_congruent:
   "(\<lambda>(a, b). {of_int a / of_int b :: 'a::field_char_0}) respects ratrel"
-apply (rule congruent.intro)
+apply (rule congruentI)
 apply (clarsimp simp add: nonzero_divide_eq_eq nonzero_eq_divide_eq)
 apply (simp only: of_int_mult [symmetric])
 done