updated functor Named_Thms;
updated type attribute;

--- a/doc-src/IsarImplementation/Thy/Isar.thy	Tue Nov 08 22:22:59 2011 +0100
+++ b/doc-src/IsarImplementation/Thy/Isar.thy	Tue Nov 08 22:38:56 2011 +0100
@@ -449,7 +449,7 @@
 ML {*
   structure My_Simps =
     Named_Thms
-      (val name = "my_simp" val description = "my_simp rule")
+      (val name = @{binding my_simp} val description = "my_simp rule")
 *}
 setup My_Simps.setup
 
@@ -516,10 +516,10 @@
 
 text {* An \emph{attribute} is a function @{text "context \<times> thm \<rightarrow>
   context \<times> thm"}, which means both a (generic) context and a theorem
-  can be modified simultaneously.  In practice this fully general form
-  is very rare, instead attributes are presented either as
-  \emph{declaration attribute:} @{text "thm \<rightarrow> context \<rightarrow> context"} or
-  \emph{rule attribute:} @{text "context \<rightarrow> thm \<rightarrow> thm"}.
+  can be modified simultaneously.  In practice this mixed form is very
+  rare, instead attributes are presented either as \emph{declaration
+  attribute:} @{text "thm \<rightarrow> context \<rightarrow> context"} or \emph{rule
+  attribute:} @{text "context \<rightarrow> thm \<rightarrow> thm"}.
 
   Attributes can have additional arguments via concrete syntax.  There
   is a collection of context-sensitive parsers for various logical
@@ -535,7 +535,7 @@
 
 text %mlref {*
   \begin{mldecls}
-  @{index_ML_type attribute: "Context.generic * thm -> Context.generic * thm"} \\
+  @{index_ML_type attribute} \\
   @{index_ML Thm.rule_attribute: "(Context.generic -> thm -> thm) -> attribute"} \\
   @{index_ML Thm.declaration_attribute: "
   (thm -> Context.generic -> Context.generic) -> attribute"} \\

--- a/doc-src/IsarImplementation/Thy/document/Isar.tex	Tue Nov 08 22:22:59 2011 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Isar.tex	Tue Nov 08 22:38:56 2011 +0100
@@ -724,7 +724,11 @@
 \ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline
 \ \ structure\ My{\isaliteral{5F}{\isacharunderscore}}Simps\ {\isaliteral{3D}{\isacharequal}}\isanewline
 \ \ \ \ Named{\isaliteral{5F}{\isacharunderscore}}Thms\isanewline
-\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}val\ name\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}my{\isaliteral{5F}{\isacharunderscore}}simp{\isaliteral{22}{\isachardoublequote}}\ val\ description\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}my{\isaliteral{5F}{\isacharunderscore}}simp\ rule{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}\isanewline
+\ \ \ \ \ \ {\isaliteral{28}{\isacharparenleft}}val\ name\ {\isaliteral{3D}{\isacharequal}}\ %
+\isaantiq
+binding\ my{\isaliteral{5F}{\isacharunderscore}}simp{}%
+\endisaantiq
+\ val\ description\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequote}}my{\isaliteral{5F}{\isacharunderscore}}simp\ rule{\isaliteral{22}{\isachardoublequote}}{\isaliteral{29}{\isacharparenright}}\isanewline
 {\isaliteral{2A7D}{\isacharverbatimclose}}\isanewline
 \isacommand{setup}\isamarkupfalse%
 \ My{\isaliteral{5F}{\isacharunderscore}}Simps{\isaliteral{2E}{\isachardot}}setup%
@@ -835,10 +839,10 @@
 %
 \begin{isamarkuptext}%
 An \emph{attribute} is a function \isa{context\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ thm\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ context\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ thm}, which means both a (generic) context and a theorem
-  can be modified simultaneously.  In practice this fully general form
-  is very rare, instead attributes are presented either as
-  \emph{declaration attribute:} \isa{thm\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ context} or
-  \emph{rule attribute:} \isa{context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ thm\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ thm}.
+  can be modified simultaneously.  In practice this mixed form is very
+  rare, instead attributes are presented either as \emph{declaration
+  attribute:} \isa{thm\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ context} or \emph{rule
+  attribute:} \isa{context\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ thm\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ thm}.
 
   Attributes can have additional arguments via concrete syntax.  There
   is a collection of context-sensitive parsers for various logical
@@ -862,7 +866,7 @@
 %
 \begin{isamarkuptext}%
 \begin{mldecls}
-  \indexdef{}{ML type}{attribute}\verb|type attribute = Context.generic * thm -> Context.generic * thm| \\
+  \indexdef{}{ML type}{attribute}\verb|type attribute| \\
   \indexdef{}{ML}{Thm.rule\_attribute}\verb|Thm.rule_attribute: (Context.generic -> thm -> thm) -> attribute| \\
   \indexdef{}{ML}{Thm.declaration\_attribute}\verb|Thm.declaration_attribute: |\isasep\isanewline%
 \verb|  (thm -> Context.generic -> Context.generic) -> attribute| \\