# HG changeset patch
# User wenzelm
# Date 1372074897 -7200
# Node ID c54e551de6f914965d95618f5a2072b2e06522fd
# Parent  6646bb548c6b8dfc65730bc66154d8af343baaad
tuned;

diff -r 6646bb548c6b -r c54e551de6f9 src/Doc/IsarImplementation/Logic.thy
--- 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