command 'defaultsort' is renamed to 'default_sort', it works within a local theory context;

--- a/NEWS	Wed Apr 28 12:18:49 2010 +0200
+++ b/NEWS	Wed Apr 28 12:21:55 2010 +0200
@@ -116,6 +116,9 @@
 context -- without introducing dependencies on parameters or
 assumptions, which is not possible in Isabelle/Pure.
 
+* Command 'defaultsort' is renamed to 'default_sort', it works within
+a local theory context.  Minor INCOMPATIBILITY.
+
 * Proof terms: Type substitutions on proof constants now use canonical
 order of type variables. INCOMPATIBILITY: Tools working with proof
 terms may need to be adapted.

--- a/doc-src/IsarRef/Thy/Spec.thy	Wed Apr 28 12:18:49 2010 +0200
+++ b/doc-src/IsarRef/Thy/Spec.thy	Wed Apr 28 12:21:55 2010 +0200
@@ -902,7 +902,7 @@
   \begin{matharray}{rcll}
     @{command_def "classes"} & : & @{text "theory \<rightarrow> theory"} \\
     @{command_def "classrel"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
-    @{command_def "defaultsort"} & : & @{text "theory \<rightarrow> theory"} \\
+    @{command_def "default_sort"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   \end{matharray}
 
@@ -911,7 +911,7 @@
     ;
     'classrel' (nameref ('<' | subseteq) nameref + 'and')
     ;
-    'defaultsort' sort
+    'default\_sort' sort
     ;
   \end{rail}
 
@@ -929,7 +929,7 @@
   (see \secref{sec:class}) provide a way to introduce proven class
   relations.
 
-  \item @{command "defaultsort"}~@{text s} makes sort @{text s} the
+  \item @{command "default_sort"}~@{text s} makes sort @{text s} the
   new default sort for any type variable that is given explicitly in
   the text, but lacks a sort constraint (wrt.\ the current context).
   Type variables generated by type inference are not affected.

--- a/doc-src/IsarRef/Thy/document/Spec.tex	Wed Apr 28 12:18:49 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Wed Apr 28 12:21:55 2010 +0200
@@ -937,7 +937,7 @@
 \begin{matharray}{rcll}
     \indexdef{}{command}{classes}\hypertarget{command.classes}{\hyperlink{command.classes}{\mbox{\isa{\isacommand{classes}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
     \indexdef{}{command}{classrel}\hypertarget{command.classrel}{\hyperlink{command.classrel}{\mbox{\isa{\isacommand{classrel}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} & (axiomatic!) \\
-    \indexdef{}{command}{defaultsort}\hypertarget{command.defaultsort}{\hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}} & : & \isa{{\isachardoublequote}theory\ {\isasymrightarrow}\ theory{\isachardoublequote}} \\
+    \indexdef{}{command}{default\_sort}\hypertarget{command.default-sort}{\hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isacharunderscore}sort}}}}} & : & \isa{{\isachardoublequote}local{\isacharunderscore}theory\ {\isasymrightarrow}\ local{\isacharunderscore}theory{\isachardoublequote}} \\
     \indexdef{}{command}{class\_deps}\hypertarget{command.class-deps}{\hyperlink{command.class-deps}{\mbox{\isa{\isacommand{class{\isacharunderscore}deps}}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isa{{\isachardoublequote}context\ {\isasymrightarrow}{\isachardoublequote}} \\
   \end{matharray}
 
@@ -946,7 +946,7 @@
     ;
     'classrel' (nameref ('<' | subseteq) nameref + 'and')
     ;
-    'defaultsort' sort
+    'default\_sort' sort
     ;
   \end{rail}
 
@@ -964,7 +964,7 @@
   (see \secref{sec:class}) provide a way to introduce proven class
   relations.
 
-  \item \hyperlink{command.defaultsort}{\mbox{\isa{\isacommand{defaultsort}}}}~\isa{s} makes sort \isa{s} the
+  \item \hyperlink{command.default-sort}{\mbox{\isa{\isacommand{default{\isacharunderscore}sort}}}}~\isa{s} makes sort \isa{s} the
   new default sort for any type variable that is given explicitly in
   the text, but lacks a sort constraint (wrt.\ the current context).
   Type variables generated by type inference are not affected.