src/HOL/Groups.thy

--- a/src/HOL/Groups.thy	Tue Aug 23 19:49:21 2011 +0200
+++ b/src/HOL/Groups.thy	Mon Aug 22 23:39:05 2011 +0200
@@ -103,11 +103,6 @@
 
 hide_const (open) zero one
 
-syntax
-  "_index1"  :: index    ("\<^sub>1")
-translations
-  (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
-
 lemma Let_0 [simp]: "Let 0 f = f 0"
   unfolding Let_def ..