diff -r 383fd113baae -r b49bd5d9041f src/Doc/Isar_Ref/Proof.thy
--- a/src/Doc/Isar_Ref/Proof.thy	Fri Sep 24 22:44:13 2021 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy	Sun Sep 26 18:49:55 2021 +0200
@@ -1321,7 +1321,6 @@
   \begin{matharray}{rcl}
     @{command_def "consider"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\
     @{command_def "obtain"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\
-    @{command_def "guess"}\<open>\<^sup>*\<close> & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\
   \end{matharray}
 
   Generalized elimination means that hypothetical parameters and premises may
@@ -1352,8 +1351,6 @@
     concl: (@{syntax props} + @'and')
     ;
     prems: (@'if' (@{syntax props'} + @'and'))?
-    ;
-    @@{command guess} @{syntax vars}
   \<close>
 
   \<^descr> @{command consider}~\<open>(a) \<^vec>x \<WHERE> \<^vec>A \<^vec>x | (b)
@@ -1412,29 +1409,14 @@
     \quad @{command "fix"}~\<open>\<^vec>x\<close>~@{command "assume"}\<open>\<^sup>* a: \<^vec>A \<^vec>x\<close> \\
   \end{matharray}
 
-  \<^descr> @{command guess} is similar to @{command obtain}, but it derives the
-  obtained context elements from the course of tactical reasoning in the
-  proof. Thus it can considerably obscure the proof: it is classified as
-  \<^emph>\<open>improper\<close>.
-
-  A proof with @{command guess} starts with a fixed goal \<open>thesis\<close>. The
-  subsequent refinement steps may turn this to anything of the form
-  \<open>\<And>\<^vec>x. \<^vec>A \<^vec>x \<Longrightarrow> thesis\<close>, but without splitting into new
-  subgoals. The final goal state is then used as reduction rule for the obtain
-  pattern described above. Obtained parameters \<open>\<^vec>x\<close> are marked as
-  internal by default, and thus inaccessible in the proof text. The variable
-  names and type constraints given as arguments for @{command "guess"} specify
-  a prefix of accessible parameters.
-
-
   In the proof of @{command consider} and @{command obtain} the local premises
   are always bound to the fact name @{fact_ref that}, according to structured
   Isar statements involving @{keyword_ref "if"} (\secref{sec:goals}).
 
-  Facts that are established by @{command "obtain"} and @{command "guess"} may
-  not be polymorphic: any type-variables occurring here are fixed in the
-  present context. This is a natural consequence of the role of @{command fix}
-  and @{command assume} in these constructs.
+  Facts that are established by @{command "obtain"} cannot be polymorphic: any
+  type-variables occurring here are fixed in the present context. This is a
+  natural consequence of the role of @{command fix} and @{command assume} in
+  this construct.
 \<close>
 
 end