tuned;

--- a/src/Doc/IsarRef/Generic.thy	Thu Nov 08 20:18:34 2012 +0100
+++ b/src/Doc/IsarRef/Generic.thy	Thu Nov 08 20:20:38 2012 +0100
@@ -602,10 +602,10 @@
 
 text {*
   \begin{matharray}{rcl}
-    @{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{attribute_def simp} & : & @{text attribute} \\
     @{attribute_def split} & : & @{text attribute} \\
     @{attribute_def cong} & : & @{text attribute} \\
+    @{command_def "print_simpset"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   \end{matharray}
 
   @{rail "
@@ -615,21 +615,6 @@
 
   \begin{description}
 
-  \item @{command "print_simpset"} prints the collection of rules
-  declared to the Simplifier, which is also known as ``simpset''
-  internally.
-
-  For historical reasons, simpsets may occur independently from the
-  current context, but are conceptually dependent on it.  When the
-  Simplifier is invoked via one of its main entry points in the Isar
-  source language (as proof method \secref{sec:simp-meth} or rule
-  attribute \secref{sec:simp-meth}), its simpset is derived from the
-  current proof context, and carries a back-reference to that for
-  other tools that might get invoked internally (e.g.\ simplification
-  procedures \secref{sec:simproc}).  A mismatch of the context of the
-  simpset and the context of the problem being simplified may lead to
-  unexpected results.
-
   \item @{attribute simp} declares rewrite rules, by adding or
   deleting them from the simpset within the theory or proof context.
   Rewrite rules are theorems expressing some form of equality, for
@@ -731,6 +716,21 @@
   This can make simplification much faster, but may require an extra
   case split over the condition @{text "?q"} to prove the goal.
 
+  \item @{command "print_simpset"} prints the collection of rules
+  declared to the Simplifier, which is also known as ``simpset''
+  internally.
+
+  For historical reasons, simpsets may occur independently from the
+  current context, but are conceptually dependent on it.  When the
+  Simplifier is invoked via one of its main entry points in the Isar
+  source language (as proof method \secref{sec:simp-meth} or rule
+  attribute \secref{sec:simp-meth}), its simpset is derived from the
+  current proof context, and carries a back-reference to that for
+  other tools that might get invoked internally (e.g.\ simplification
+  procedures \secref{sec:simproc}).  A mismatch of the context of the
+  simpset and the context of the problem being simplified may lead to
+  unexpected results.
+
   \end{description}
 
   The implicit simpset of the theory context is propagated