--- a/src/HOL/IsaMakefile Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/IsaMakefile Wed Feb 10 14:12:02 2010 +0100
@@ -397,7 +397,6 @@
Library/Library/document/root.tex Library/Library/document/root.bib \
Library/Transitive_Closure_Table.thy Library/While_Combinator.thy \
Library/Product_ord.thy Library/Char_nat.thy \
- Library/Structure_Syntax.thy \
Library/Sublist_Order.thy Library/List_lexord.thy \
Library/Coinductive_List.thy Library/AssocList.thy \
Library/Formal_Power_Series.thy Library/Binomial.thy \
--- a/src/HOL/Library/Library.thy Wed Feb 10 14:12:02 2010 +0100
+++ b/src/HOL/Library/Library.thy Wed Feb 10 14:12:02 2010 +0100
@@ -51,7 +51,6 @@
RBT
SML_Quickcheck
State_Monad
- Structure_Syntax
Sum_Of_Squares
Transitive_Closure_Table
Univ_Poly
--- a/src/HOL/Library/Structure_Syntax.thy Wed Feb 10 14:12:02 2010 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-(* Author: Florian Haftmann, TU Muenchen *)
-
-header {* Index syntax for structures *}
-
-theory Structure_Syntax
-imports Pure
-begin
-
-syntax
- "_index1" :: index ("\<^sub>1")
-translations
- (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
-
-end