1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Wed Apr 28 12:18:49 2010 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Wed Apr 28 12:21:55 2010 +0200
     1.3 @@ -902,7 +902,7 @@
     1.4    \begin{matharray}{rcll}
     1.5      @{command_def "classes"} & : & @{text "theory \<rightarrow> theory"} \\
     1.6      @{command_def "classrel"} & : & @{text "theory \<rightarrow> theory"} & (axiomatic!) \\
     1.7 -    @{command_def "defaultsort"} & : & @{text "theory \<rightarrow> theory"} \\
     1.8 +    @{command_def "default_sort"} & : & @{text "local_theory \<rightarrow> local_theory"} \\
     1.9      @{command_def "class_deps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
    1.10    \end{matharray}
    1.11  
    1.12 @@ -911,7 +911,7 @@
    1.13      ;
    1.14      'classrel' (nameref ('<' | subseteq) nameref + 'and')
    1.15      ;
    1.16 -    'defaultsort' sort
    1.17 +    'default\_sort' sort
    1.18      ;
    1.19    \end{rail}
    1.20  
    1.21 @@ -929,7 +929,7 @@
    1.22    (see \secref{sec:class}) provide a way to introduce proven class
    1.23    relations.
    1.24  
    1.25 -  \item @{command "defaultsort"}~@{text s} makes sort @{text s} the
    1.26 +  \item @{command "default_sort"}~@{text s} makes sort @{text s} the
    1.27    new default sort for any type variable that is given explicitly in
    1.28    the text, but lacks a sort constraint (wrt.\ the current context).
    1.29    Type variables generated by type inference are not affected.