src/HOL/Int.thy

--- a/src/HOL/Int.thy	Mon Mar 02 08:26:03 2009 +0100
+++ b/src/HOL/Int.thy	Mon Mar 02 16:53:55 2009 +0100
@@ -77,7 +77,7 @@
 by (simp add: intrel_def)
 
 lemma equiv_intrel: "equiv UNIV intrel"
-by (simp add: intrel_def equiv_def refl_def sym_def trans_def)
+by (simp add: intrel_def equiv_def refl_on_def sym_def trans_def)
 
 text{*Reduces equality of equivalence classes to the @{term intrel} relation:
   @{term "(intrel `` {x} = intrel `` {y}) = ((x,y) \<in> intrel)"} *}