--- a/src/Doc/IsarImplementation/Logic.thy Sun Jun 23 21:16:07 2013 +0200
+++ b/src/Doc/IsarImplementation/Logic.thy Mon Jun 24 13:54:57 2013 +0200
@@ -1352,6 +1352,7 @@
@{index_ML_op "%"}, @{index_ML_op "%%"}, @{index_ML PBound},
@{index_ML MinProof}, @{index_ML Hyp}, @{index_ML PAxm}, @{index_ML
Oracle}, @{index_ML Promise}, @{index_ML PThm} as explained above.
+ %FIXME OfClass (!?)
\item Type @{ML_type proof_body} represents the nested proof
information of a named theorem, consisting of a digest of oracles