diff -r e7e12555e763 -r e790a5560834 doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Mon Sep 06 22:08:49 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Mon Sep 06 22:31:54 2010 +0200
@@ -55,7 +55,7 @@
     ;
     ( 'prf' | 'full\_prf' ) modes? thmrefs?
     ;
-    'pr' modes? nat? (',' nat)?
+    'pr' modes? nat?
     ;
 
     modes: '(' (name + ) ')'
@@ -90,11 +90,11 @@
   compact proof term, which is denoted by ``\isa{{\isacharunderscore}}'' placeholders
   there.
 
-  \item \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}goals{\isacharcomma}\ prems{\isachardoublequote}} prints the current
-  proof state (if present), including the proof context, current facts
-  and goals.  The optional limit arguments affect the number of goals
-  and premises to be displayed, which is initially 10 for both.
-  Omitting limit values leaves the current setting unchanged.
+  \item \hyperlink{command.pr}{\mbox{\isa{\isacommand{pr}}}}~\isa{{\isachardoublequote}goals{\isachardoublequote}} prints the current proof state
+  (if present), including current facts and goals.  The optional limit
+  arguments affect the number of goals to be displayed, which is
+  initially 10.  Omitting limit value leaves the current setting
+  unchanged.
 
   \end{description}