diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Equiv_Relations.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -164,7 +164,8 @@
   assumes congruent: "(y,z) \<in> r ==> f y = f z"
 
 abbreviation
-  RESPECTS :: "('a => 'b) => ('a * 'a) set => bool"  (infixr "respects" 80)
+  RESPECTS :: "('a => 'b) => ('a * 'a) set => bool"
+    (infixr "respects" 80) where
   "f respects r == congruent r f"
 
 
@@ -222,7 +223,8 @@
 
 text{*Abbreviation for the common case where the relations are identical*}
 abbreviation
-  RESPECTS2:: "['a => 'a => 'b, ('a * 'a)set] => bool" (infixr "respects2 " 80)
+  RESPECTS2:: "['a => 'a => 'b, ('a * 'a) set] => bool"
+    (infixr "respects2 " 80) where
   "f respects2 r == congruent2 r r f"