1.1 --- a/doc-src/IsarRef/Thy/Spec.thy	Thu Jan 22 09:04:45 2009 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Spec.thy	Thu Jan 22 09:04:45 2009 +0100
     1.3 @@ -436,7 +436,6 @@
     1.4    \begin{matharray}{rcl}
     1.5      @{command_def "interpretation"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
     1.6      @{command_def "interpret"} & : & @{text "proof(state) | proof(chain \<rightarrow> proof(prove)"} \\
     1.7 -    @{command_def "print_interps"}@{text "\<^sup>*"} & : &  @{text "context \<rightarrow>"} \\
     1.8    \end{matharray}
     1.9  
    1.10    \indexouternonterm{interp}
    1.11 @@ -445,8 +444,6 @@
    1.12      ;
    1.13      'interpret' interp
    1.14      ;
    1.15 -    'print\_interps' '!'? name
    1.16 -    ;
    1.17      instantiation: ('[' (inst+) ']')?
    1.18      ;
    1.19      interp: (name ':')? \\ (contextexpr instantiation |
    1.20 @@ -531,13 +528,6 @@
    1.21    interprets @{text expr} in the proof context and is otherwise
    1.22    similar to interpretation in theories.
    1.23  
    1.24 -  \item @{command "print_interps"}~@{text loc} prints the
    1.25 -  interpretations of a particular locale @{text loc} that are active
    1.26 -  in the current context, either theory or proof context.  The
    1.27 -  exclamation point argument triggers printing of \emph{witness}
    1.28 -  theorems justifying interpretations.  These are normally omitted
    1.29 -  from the output.
    1.30 -  
    1.31    \end{description}
    1.32  
    1.33    \begin{warn}