1.1 --- a/src/HOL/IsaMakefile	Wed Feb 10 14:12:02 2010 +0100
     1.2 +++ b/src/HOL/IsaMakefile	Wed Feb 10 14:12:02 2010 +0100
     1.3 @@ -397,7 +397,6 @@
     1.4    Library/Library/document/root.tex Library/Library/document/root.bib	\
     1.5    Library/Transitive_Closure_Table.thy Library/While_Combinator.thy	\
     1.6    Library/Product_ord.thy Library/Char_nat.thy				\
     1.7 -  Library/Structure_Syntax.thy						\
     1.8    Library/Sublist_Order.thy Library/List_lexord.thy			\
     1.9    Library/Coinductive_List.thy Library/AssocList.thy			\
    1.10    Library/Formal_Power_Series.thy Library/Binomial.thy			\

     2.1 --- a/src/HOL/Library/Library.thy	Wed Feb 10 14:12:02 2010 +0100
     2.2 +++ b/src/HOL/Library/Library.thy	Wed Feb 10 14:12:02 2010 +0100
     2.3 @@ -51,7 +51,6 @@
     2.4    RBT
     2.5    SML_Quickcheck
     2.6    State_Monad
     2.7 -  Structure_Syntax
     2.8    Sum_Of_Squares
     2.9    Transitive_Closure_Table
    2.10    Univ_Poly

     3.1 --- a/src/HOL/Library/Structure_Syntax.thy	Wed Feb 10 14:12:02 2010 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,14 +0,0 @@
     3.4 -(* Author: Florian Haftmann, TU Muenchen *)
     3.5 -
     3.6 -header {* Index syntax for structures *}
     3.7 -
     3.8 -theory Structure_Syntax
     3.9 -imports Pure
    3.10 -begin
    3.11 -
    3.12 -syntax
    3.13 -  "_index1"  :: index    ("\<^sub>1")
    3.14 -translations
    3.15 -  (index) "\<^sub>1" => (index) "\<^bsub>\<struct>\<^esub>"
    3.16 -
    3.17 -end