diff -r bf84bdf05f14 -r ec5cd5b1804c src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Thu Mar 23 18:14:06 2006 +0100
+++ b/src/HOL/Equiv_Relations.thy	Thu Mar 23 20:03:53 2006 +0100
@@ -163,11 +163,9 @@
   fixes r and f
   assumes congruent: "(y,z) \<in> r ==> f y = f z"
 
-syntax
-  RESPECTS ::"['a => 'b, ('a * 'a) set] => bool"  (infixr "respects" 80)
-
-translations
-  "f respects r" == "congruent r f"
+abbreviation (output)
+  RESPECTS :: "('a => 'b) => ('a * 'a) set => bool"  (infixr "respects" 80)
+  "f respects r = congruent r f"
 
 
 lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. f y = c ==> (\<Union>y \<in> A. f(y))=c"
@@ -225,9 +223,12 @@
 text{*Abbreviation for the common case where the relations are identical*}
 syntax
   RESPECTS2 ::"['a => 'b, ('a * 'a) set] => bool"  (infixr "respects2 " 80)
-
 translations
   "f respects2 r" => "congruent2 r r f"
+(*
+Warning: cannot use "abbreviation" here because the two occurrences of
+r may need to be of different type (see Hyperreal/StarDef).
+*)
 
 lemma congruent2_implies_congruent:
     "equiv A r1 ==> congruent2 r1 r2 f ==> a \<in> A ==> congruent r2 (f a)"
@@ -333,7 +334,7 @@
  apply(fastsimp simp add:inj_on_def)
 apply (simp add:setsum_constant)
 done
-
+(*
 ML
 {*
 val UN_UN_split_split_eq = thm "UN_UN_split_split_eq";
@@ -371,5 +372,5 @@
 val subset_equiv_class = thm "subset_equiv_class";
 val sym_trans_comp_subset = thm "sym_trans_comp_subset";
 *}
-
+*)
 end