# HG changeset patch
# User wenzelm
# Date 1662635806 -7200
# Node ID 3f5028b5441914d6422b235399f51222d305054b
# Parent  315a6b0b6173491d68f3f164e0c54d0dbbf415ef
removed odd TODO item (see 3391a493f39a);

diff -r 315a6b0b6173 -r 3f5028b54419 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Sep 08 13:13:40 2022 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Sep 08 13:16:46 2022 +0200
@@ -1334,7 +1334,7 @@
 end;
 
 
-(* terminal proofs *)  (* FIXME avoid toplevel imitation -- include in PIDE/document *)
+(* terminal proofs *)
 
 local