diff -r 4319691be975 -r 3dec88149176 src/Doc/IsarRef/Proof.thy
--- a/src/Doc/IsarRef/Proof.thy	Mon Nov 19 18:01:48 2012 +0100
+++ b/src/Doc/IsarRef/Proof.thy	Mon Nov 19 20:23:47 2012 +0100
@@ -670,9 +670,9 @@
   pretending to solve the pending claim without further ado.  This
   only works in interactive development, or if the @{ML
   quick_and_dirty} flag is enabled (in ML).  Facts emerging from fake
-  proofs are not the real thing.  Internally, each theorem container
-  is tainted by an oracle invocation, which is indicated as ``@{text
-  "[!]"}'' in the printed result.
+  proofs are not the real thing.  Internally, the derivation object is
+  tainted by an oracle invocation, which may be inspected via the
+  theorem status \cite{isabelle-implementation}.
   
   The most important application of @{command "sorry"} is to support
   experimentation and top-down proof development.