# HG changeset patch
# User wenzelm
# Date 1452339307 -3600
# Node ID f74a33b14200ece4de283066533a8fe8bd71f722
# Parent  d6af554512d74d783034d5074e5a7beb12a23db6
discontinued \<struct> syntax;

diff -r d6af554512d7 -r f74a33b14200 NEWS
--- a/NEWS	Fri Jan 08 20:06:48 2016 +0100
+++ b/NEWS	Sat Jan 09 12:35:07 2016 +0100
@@ -342,6 +342,10 @@
 * Keyword 'rewrites' identifies rewrite morphisms in interpretation
 commands. Previously, the keyword was 'where'. INCOMPATIBILITY.
 
+* Special notation \<struct> for the first implicit 'structure' in the context
+has been discontinued. Rare INCOMPATIBILITY, use explicit structure name
+instead, notably in indexed notation with block-subscript (e.g. \<odot>\<^bsub>A\<^esub>).
+
 * More gentle suppression of syntax along locale morphisms while
 printing terms. Previously 'abbreviation' and 'notation' declarations
 would be suppressed for morphisms except term identity. Now
diff -r d6af554512d7 -r f74a33b14200 src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Fri Jan 08 20:06:48 2016 +0100
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Jan 09 12:35:07 2016 +0100
@@ -656,7 +656,6 @@
     & \<open>|\<close> & \<^verbatim>\<open>CONST\<close> \<open>id  |\<close>~~\<^verbatim>\<open>CONST\<close> \<open>longid\<close> \\
     & \<open>|\<close> & \<^verbatim>\<open>XCONST\<close> \<open>id  |\<close>~~\<^verbatim>\<open>XCONST\<close> \<open>longid\<close> \\
     & \<open>|\<close> & \<open>logic\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)  any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>) \<dots> any\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> & \<open>(999)\<close> \\
-    & \<open>|\<close> & \<open>\<struct> index\<^sup>(\<^sup>1\<^sup>0\<^sup>0\<^sup>0\<^sup>)\<close> \\
     & \<open>|\<close> & \<^verbatim>\<open>%\<close> \<open>pttrns\<close> \<^verbatim>\<open>.\<close> \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\
     & \<open>|\<close> & \<open>\<lambda>\<close> \<open>pttrns\<close> \<^verbatim>\<open>.\<close> \<open>any\<^sup>(\<^sup>3\<^sup>)\<close> & \<open>(3)\<close> \\
     & \<open>|\<close> & \<^verbatim>\<open>op\<close> \<^verbatim>\<open>==\<close>~~\<open>|\<close>~~\<^verbatim>\<open>op\<close> \<open>\<equiv>\<close>~~\<open>|\<close>~~\<^verbatim>\<open>op\<close> \<^verbatim>\<open>&&&\<close> \\
diff -r d6af554512d7 -r f74a33b14200 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Fri Jan 08 20:06:48 2016 +0100
+++ b/src/Pure/pure_thy.ML	Sat Jan 09 12:35:07 2016 +0100
@@ -151,7 +151,7 @@
     ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
     ("_indexdefault", typ "index",                     Delimfix ""),
     ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
-    ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
+    ("_struct",     typ "index => logic",              NoSyn),
     ("_update_name", typ "idt",                        NoSyn),
     ("_constrainAbs", typ "'a",                        NoSyn),
     ("_position_sort", typ "tid => tid_position",      Delimfix "_"),