diff -r c06f1d36a8c9 -r dedd7952a62c src/Doc/IsarImplementation/Logic.thy
--- a/src/Doc/IsarImplementation/Logic.thy	Thu Jun 27 20:09:39 2013 +0200
+++ b/src/Doc/IsarImplementation/Logic.thy	Thu Jun 27 23:17:26 2013 +0200
@@ -1335,7 +1335,6 @@
   \begin{mldecls}
   @{index_ML_type proof} \\
   @{index_ML_type proof_body} \\
-  @{index_ML proofs: "int Unsynchronized.ref"} \\
   @{index_ML Reconstruct.reconstruct_proof:
   "theory -> term -> proof -> proof"} \\
   @{index_ML Reconstruct.expand_proof: "theory ->
@@ -1345,6 +1344,10 @@
   @{index_ML Proof_Syntax.pretty_proof: "Proof.context -> proof -> Pretty.T"} \\
   \end{mldecls}
 
+  \begin{tabular}{rcll}
+  @{attribute_def proofs} & : & @{text attribute} & default @{text 1} \\
+  \end{tabular}
+
   \begin{description}
 
   \item Type @{ML_type proof} represents proof terms; this is a
@@ -1370,13 +1373,6 @@
   Parallel performance may suffer by inspecting proof terms at
   run-time.
 
-  \item @{ML proofs} specifies the detail of proof recording within
-  @{ML_type thm} values produced by the inference kernel: @{ML 0}
-  records only the names of oracles, @{ML 1} records oracle names and
-  propositions, @{ML 2} additionally records full proof terms.
-  Officially named theorems that contribute to a result are recorded
-  in any case.
-
   \item @{ML Reconstruct.reconstruct_proof}~@{text "thy prop prf"}
   turns the implicit proof term @{text "prf"} into a full proof of the
   given proposition.
@@ -1404,6 +1400,13 @@
   \item @{ML Proof_Syntax.pretty_proof}~@{text "ctxt prf"}
   pretty-prints the given proof term.
 
+  \item @{attribute proofs} specifies the detail of proof recording within
+  @{ML_type thm} values produced by the inference kernel: @{text 0}
+  records only the names of oracles, @{text 1} records oracle names and
+  propositions, @{text 2} additionally records full proof terms.
+  Officially named theorems that contribute to a result are recorded
+  in any case.  %FIXME move to IsarRef
+
   \end{description}
 *}