From 6d570f591af3d4aa5ded571cea0b70bd83e362fa Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 3 Nov 1998 14:40:52 +0000
Subject: Note added.

---
 generic/proof-script.el | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'generic/proof-script.el')

diff --git a/generic/proof-script.el b/generic/proof-script.el
index cefcbd39..93e54789 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -553,7 +553,8 @@ the ACS is marked in the current buffer. If CMD does not match any,
 	      (setq nam (match-string 2 (span-property gspan 'cmd)))
 	    ;; This only works for Coq, but LEGO raises an error if
 	    ;; there's no name.
-	    ;; FIXME: a nonsense for Isabelle.
+	    ;; FIXME da: maybe this should be prover specific: is
+	    ;; "Unnamed_thm" actually a Coq identifier?
 	    (setq nam "Unnamed_thm")))
 
       (set-span-end gspan end)
-- 
cgit v1.2.3