--- 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
--- 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> \\
--- 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 "_"),