--- a/src/Doc/IsarRef/Proof.thy Fri May 17 20:30:04 2013 +0200
+++ b/src/Doc/IsarRef/Proof.thy Fri May 17 20:41:45 2013 +0200
@@ -668,8 +668,8 @@
\item @{command "sorry"} is a \emph{fake proof}\index{proof!fake}
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
+ only works in interactive development, or if the @{attribute
+ quick_and_dirty} is enabled. Facts emerging from fake
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}.