src/HOL/GroupTheory/Ring.thy

--- a/src/HOL/GroupTheory/Ring.thy	Mon Dec 10 20:58:15 2001 +0100
+++ b/src/HOL/GroupTheory/Ring.thy	Mon Dec 10 20:59:43 2001 +0100
@@ -42,7 +42,7 @@
 
 constdefs
   group_of :: "'a ringtype => 'a grouptype"
-   "group_of == lam R: Ring. (| carrier = (R.<cr>), bin_op = (R.<f>),
+   "group_of == %R: Ring. (| carrier = (R.<cr>), bin_op = (R.<f>),
 			        inverse = (R.<inv>), unit = (R.<e>) |)"
 
 locale ring = group +