# HG changeset patch
# User wenzelm
# Date 1316467472 -7200
# Node ID 11a542f50fc33cd89892c1778d9931b6f9d5eee4
# Parent  0d2d59525912ab2ea428ba07e30ec66f138da4ec
less ambiguous syntax;

diff -r 0d2d59525912 -r 11a542f50fc3 src/HOL/Algebra/AbelCoset.thy
--- a/src/HOL/Algebra/AbelCoset.thy	Mon Sep 19 23:18:18 2011 +0200
+++ b/src/HOL/Algebra/AbelCoset.thy	Mon Sep 19 23:24:32 2011 +0200
@@ -36,7 +36,7 @@
   where "A_SET_INV G H = SET_INV \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr> H"
 
 definition
-  a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("racong\<index> _")
+  a_r_congruent :: "[('a,'b)ring_scheme, 'a set] \<Rightarrow> ('a*'a)set"  ("racong\<index>")
   where "a_r_congruent G = r_congruent \<lparr>carrier = carrier G, mult = add G, one = zero G\<rparr>"
 
 definition