diff -r 0390abdd1e62 -r 02b8f3bcf7fe src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Thu Apr 22 11:00:22 2004 +0200
+++ b/src/HOL/Algebra/Coset.thy	Thu Apr 22 11:01:34 2004 +0200
@@ -9,23 +9,23 @@
 
 declare (in group) l_inv [simp]  r_inv [simp] 
 
-constdefs
-  r_coset    :: "[('a,'b) monoid_scheme,'a set, 'a] => 'a set"    
-   "r_coset G H a == (% x. (mult G) x a) ` H"
+constdefs (structure G)
+  r_coset    :: "[_,'a set, 'a] => 'a set"    
+   "r_coset G H a == (% x. x \<otimes> a) ` H"
 
-  l_coset    :: "[('a,'b) monoid_scheme, 'a, 'a set] => 'a set"
-   "l_coset G a H == (% x. (mult G) a x) ` H"
+  l_coset    :: "[_, 'a, 'a set] => 'a set"
+   "l_coset G a H == (% x. a \<otimes> x) ` H"
 
-  rcosets  :: "[('a,'b) monoid_scheme,'a set] => ('a set)set"
+  rcosets  :: "[_, 'a set] => ('a set)set"
    "rcosets G H == r_coset G H ` (carrier G)"
 
-  set_mult  :: "[('a,'b) monoid_scheme,'a set,'a set] => 'a set"
-   "set_mult G H K == (%(x,y). (mult G) x y) ` (H \<times> K)"
+  set_mult  :: "[_, 'a set ,'a set] => 'a set"
+   "set_mult G H K == (%(x,y). x \<otimes> y) ` (H \<times> K)"
 
-  set_inv   :: "[('a,'b) monoid_scheme,'a set] => 'a set"
-   "set_inv G H == (m_inv G) ` H"
+  set_inv   :: "[_,'a set] => 'a set"
+   "set_inv G H == m_inv G ` H"
 
-  normal     :: "['a set, ('a,'b) monoid_scheme] => bool"       (infixl "<|" 60)
+  normal     :: "['a set, _] => bool"       (infixl "<|" 60)
    "normal H G == subgroup H G & 
                   (\<forall>x \<in> carrier G. r_coset G H x = l_coset G x H)"