diff -r 6d93140a206c -r 93f3f9a2ae91 src/Doc/IsarImplementation/Logic.thy
--- a/src/Doc/IsarImplementation/Logic.thy	Fri Jun 21 13:36:10 2013 +0200
+++ b/src/Doc/IsarImplementation/Logic.thy	Sat Jun 22 18:24:06 2013 +0200
@@ -1148,7 +1148,7 @@
   {@{text "(\<And>\<^vec>x. \<^vec>H \<^vec>x \<Longrightarrow> A \<^vec>x) \<Longrightarrow> C"} & @{text "A\<vartheta> = H\<^sub>i\<vartheta>"}~~\text{(for some~@{text i})}}
   \]
 
-  FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution}
+  %FIXME @{inference_def elim_resolution}, @{inference_def dest_resolution}
 *}
 
 text %mlref {*