diff -r 1a38142e1172 -r 994d1a1105ef src/Doc/Isar_Ref/Inner_Syntax.thy
--- a/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Aug 06 17:39:21 2016 +0200
+++ b/src/Doc/Isar_Ref/Inner_Syntax.thy	Sat Aug 06 18:14:59 2016 +0200
@@ -84,10 +84,8 @@
     \<open>a\<^sub>1, \<dots>, a\<^sub>n\<close> do not have any permanent effect.
 
     \<^descr> @{command "prf"} displays the (compact) proof term of the current proof
-    state (if present), or of the given theorems. Note that this requires
-    proof terms to be switched on for the current object logic (see the
-    ``Proof terms'' section of the Isabelle reference manual for information
-    on how to do this).
+    state (if present), or of the given theorems. Note that this requires an
+    underlying logic image with proof terms enabled, e.g. \<open>HOL-Proofs\<close>.
 
     \<^descr> @{command "full_prf"} is like @{command "prf"}, but displays the full
     proof term, i.e.\ also displays information omitted in the compact proof