# HG changeset patch
# User wenzelm
# Date 1083441552 -7200
# Node ID f61ea8bfa81ed3353a799624a705fce75111f50a
# Parent  eafb91eda9e844ec839d33b7e18c2ab13c2203fa
_index1: accomodate improved indexed syntax;

diff -r eafb91eda9e8 -r f61ea8bfa81e src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat May 01 21:58:52 2004 +0200
+++ b/src/HOL/HOL.thy	Sat May 01 21:59:12 2004 +0200
@@ -181,7 +181,7 @@
 syntax
   "_index1"  :: index    ("\<^sub>1")
 translations
-  (index) "\<^sub>1" == "_index 1"
+  (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
 
 local